[YICES-HELP] Yices: Benchmark Expected

[Christian Dehnert]

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.