SMT Interface libraryΒΆ

This library can translate mCRL2 data expressions to SMTLIB2 format and send them to the Z3 SMT solver. An example of its use can be found in the folder libraries/smt/example.

The library still has a few limitations, among which:

  • Overloaded constructors are not supported (this is a limitation in SMTLIB2).

  • Higher-order expressions are not supported (also a limitation of SMTLIB2).

  • The library does not deal perfectly with the Pos and Nat sorts. They are both translated to the native Int type in SMTLIB2, combined with an assertion that limits their domain. However, the assertions are not complete. For example, for a function f: Pos -> Pos, the following assertion is missing:

    (forall ((p Int)) (>= (f p) 1)).