The latest release of Alt-Ergo version 2.5.1 is out, with improved SMT-LIB and bitvector support!
We are happy to announce a new release of Alt‑Ergo (version 2.5.1).
Alt-Ergo is a cutting-edge automated prover designed specifically for mathematical formulas, with a primary focus on advancing program verification.
This powerful tool is instrumental in the arsenal of static analysis solutions such as Trust-In-Soft Analyzer and Frama-C. It accompanies other major solvers like CVC5 and Z3, and is part of the solvers used behind Why3, a platform renowned for deductive program verification.
Find out more about Alt‑Ergo and how to join the Alt-Ergo Users' Club here!
This release includes the following new features and improvements:
- support for bit-vectors in the SMT-LIB format;
- new SMT-LIB parser and typechecker;
- improved bit-vector reasoning;
- partial support for SMT-LIB commands
- simplified options to enable floating-point arithmetic theory;
- various bug fixes.
Update for bug fixes
Since writing this blog post, we have released Alt-Ergo version 2.5.2 which fixes an incorrect implementation of the
(distinct) SMT-LIB operator when applied to more than two arguments, and a (rare) crash in model generation. We strongly advise users interested in SMT-LIB or model generation support upgrade to version 2.5.2 on OPAM.
Better SMT-LIB Support
This release includes a better support of the SMT-LIB standard v2.6. More precisely, the release contains:
- built-in primitives for the FixedSizeBitVectors;
- Reals_Ints theories and the QF_BV logic;
- new fully-featured parsers and type-checkers for SMT-LIB and native Alt-Ergo languages;
- specific and meaningful messages for syntax and typing errors.
These features are powered by the Dolmen Library through a new frontend alongside the legacy one. Dolmen, developed by our own Guillaume Bury, is also used by the SMT community to check the conformity of the SMT-LIB benchmarks.
In this release, the legacy frontend is still the default.
If you want to enable the new Dolmen frontend, use the option
--frontend dolmen. We encourage you to try it and report any bugs on our
Note: We plan to deprecate the legacy frontend and make Dolmen the default frontend in version
2.6.0, and to fully remove the legacy frontend in version
Support For Bit-Vectors Primitives
Alt-Ergo has had support for bit-vectors in its native language for a long time, but bit-vectors were not supported by the old SMT-LIB parser, and hence not available in the SMT-LIB format. This has changed with the new Dolmen front-end, and support for bit-vectors in the SMT-LIB format is now available starting with Alt-Ergo 2.5.1!
The SMT-LIB theories for bit-vectors,
QF_BV, have more primitives than
those previously available in Alt-Ergo. Alt-Ergo 2.5.1 supports all the
primitives in the
QF_BV primitives when using the Dolmen frontend.
Alt-Ergo's reasoning capabilities on the new primitives are limited, and will
be gradually improved in future releases.
Built-in Primitives For Mixed Integer And Real Problems
In this release, we add the support for the
is_int of the SMT-LIB theory
Notice that the support is only avalaible through the Dolmen frontend.
For instance, the input file
(set-logic ALL) (declare-const x Int) (declare-const y Real) (declare-fun f (Int Int) Int) (assert (= (f x y) 0)) (check-sat)
with the command:
alt-ergo --frontend dolmen input.smt2
produces the limpid error message:
File "input.smt2", line 5, character 11-18: 5 | (assert (= (f x y) 0)) ^^^^^^^ Error The term: `y` has type `real` but was expected to be of type `int`
Generating models (also known as counterexamples) is highly appreciated by
users of SMT-solvers. Indeed, most builtin theories in common SMT-solvers
are incomplete. As a consequence, solvers can fail to discharge goals and,
without models, the SMT-solver behaves as a black box by outputting laconic
Providing best-effort counterexamples assists developers to understand why the solver failed to validate goals. If the goal isn't valid, the solver should, as much as it can, output a correct counter-example that helps users while fixing their specifications. If the goal is actually valid, the generated model is wrong but it can help SMT-solver's maintainers to understand why their solver didn't manage to discharge the goal.
Model generation for
LIA theory and
enum theory is available in Alt-Ergo.
The feature for other theories is either in testing phase or being implemented.
If you run into wrong models, please report them on our
The present release provides convenient ways to invoking models.
Notice that we change model invocation since the post
Alt-Ergo: the SMT solver with model generation
about model generation on the
next development branch.
Check out the documentation for more details.
Floating Point Support
In version 2.5.1, the options to enable support for unbounded floating-point
arithmetic have been simplified. The options
--prelude fpa-theory-2019-10-08-19h00.ae are gone: floating-point arithmetic
is now treated as a built-in theory and can be enabled with
--enable-theories fpa. We plan on enabling support for the FPA theory by default
in a future release.
To turn on the
fpa theory, use the new option
--enable-theory fpa as follows:
alt-ergo --enable-theory fpa input.smt2
About Alt-Ergo 2.5.0
Version 2.5.0 should not be used, as it contains a soundness bug with the
bvnot primitive that slipped through the cracks. The bug was found
immediately after the release, and version 2.5.1 released with a fix.
We thank members of the Alt-Ergo Users' Club: Thales, Trust-in-Soft, AdaCore, MERCE and the CEA.
We specially thank David Mentré and Denis Cousineau at Mitsubishi Electric R&D Center Europe for funding the initial work on model generation. Note that MERCE has been a Member of the Alt-Ergo Users' Club for three years. This partnership allowed Alt-Ergo to evolve and we hope that more users will join the Club on our journey to make Alt-Ergo a must-have tool.
Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI) of the Université Paris Sud and is maintained, developed and distributed since 2013 by the company OCamlPro.
Alt-Ergo is part of the formal methods team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP and the Alt-Ergo Users' Club members. If you like Alt-Ergo, consider joining the Alt-Ergo user’s Club.