[YICES] Documentation on Yices SMT-LIB

[Bruno Dutertre]

Hormoz Zarnani wrote:
> Hello.  My name is Hormoz Zarnani, and I am a second-year computer
> science PhD student at CMU.  I am working on a C interpreter with my
> adviser, Randy Bryant, which among other things generates specifications
> in SMT-LIB format.  I have been using Yices 1.0 (which I downloaded off
> of the SMT-COMP web site) as the target for my tool.
> 
> I am wondering if there is a documentation on Yices SMT-LIB.  I wasn't
> able to find one on <http://yices.csl.sri.com/documentation.shtml> nor
> on the SMT-LIB web site.
> 
> Thanks,
> Hormoz
> 

Hormoz,

Try to use an up-to-date version of Yices by downloading it at
http://yices.csl.sri.com/. The current released version is 1.0.9 and it
includes many bug fixes. Do not use Yices 1.0.

As for the SMT-LIB documentation, it can be found on the SMT-LIB website
at http://www.smt-lib.org. You'll need to check:
- the SMT-LIB Standard Version 1.2 (click on the "Documents" link)
- the theories and logic specifications (follow the links "Theories" and "Logics")

For the most recent news and upgrades to SMT-LIB, you'll have to read
the SMT-LIB mailing list. Archived at http://www.cs.nyu.edu/pipermail/smt-lib

To use Yices on SMT-LIB problems, just use the flag -smt. Type 'yices --help'
to see what other options you can use. Also double check the documentation:
http://yices.csl.sri.com/documentation.shtml. The options are the same whether
you use SMT-LIB or the Yices language.

Regards,

Bruno