From: John Matthews <matthews@galois.com>
We are pleased to announce that ismt, our external oracle to SRI's
Yices SMT solver, is now compatible with Isabelle2009-2 and Yices
v1.0.28.
http://www.galois.com/company/open_source/ismt
The main novelty of ismt is that it communicates with Yices in Yices'
native formula language, which is richer than SMT-LIB. For example,
Isabelle datatypes are translated directly into Yices datatypes.
Enjoy!
Last updated: Nov 21 2024 at 12:39 UTC