[YICES-HELP] Yices: Benchmark Expected

[Bruno Dutertre]

Christian Dehnert wrote:
> Hi,
> 
> my name is Christian Dehnert and I am a student in Joost-Pieter Katoens 
> Verification group at RWTH Aachen. My goal is to use SMT solvers to 
> calculate abstractions for probabilistic systems. To that end, I 
> downloaded Yices 2 and wanted to play around with it a bit and 
> discovered, that I apparently cannot even produce a syntactically 
> correct input file, because Yices always complains
> 
> stdin: syntax error (line 1, column 2): benchmark expected
> 
> which I find rather surprising as it also rejects input files (giving 
> the same error message) from the benchmark suite of the SMT-LIB website 
> that it refers to as its correct form of input. Am I doing something 
> terribly wrong here?
> 
> Best regards,
> Chris
> 
> PS: I am using Mac OS 10.6 and both, the 32-bit and the 64-bit versions 
> produced that behaviour and in a virtual machine the 32-bit linux 
> version did too.
> 

Hi Chris,

The SMT LIB standard has changed in 2010. Yices 2 reads input in the
SMT-LIB notation version 1.2. It does not support SMT-LIB version 2.
So if you want to use the benchmarks provided at
http://goedel.cs.uiowa.edu/smtlib/, you'll have to get the
'Older benchmarks conforming to SMT-LIB 1,2',  The SMT-LIB 1.2
specification can be downloaded from that website too,

Bruno