SMT-LIB Version 2

Alt-Ergo has partial support for the SMT-LIB standard language from the SMT community.

Note: As of version 2.5.0, enhanced support for the SMT-LIB language is provided by the new Dolmen frontend. To use it, pass the option --frontend dolmen to Alt-Ergo. This will become the default in a future release.

Bit-vectors

Since version 2.5.0, Alt-Ergo has partial support for the FixedSizeBitVectors theory and the QF_BV and BV logics when used with the Dolmen frontend. All the symbols from these logics are available, although reasoning using them is limited and incomplete for now.

The non-standard symbols bv2nat and (_ int2bv n) (where n > 0 is a natural number representing the target bit-vector size) for conversion between integers and bit-vectors are supported.