Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ismt update


view this post on Zulip Email Gateway (Aug 18 2022 at 16:26):

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: Apr 26 2024 at 20:16 UTC