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 set-option and get-model;
• 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.

Important: 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 issue tracker.

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 2.7.0.

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, BV and QF_BV, have more primitives than those previously available in Alt-Ergo. Alt-Ergo 2.5.1 supports all the primitives in the BV and 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 primitives to_real, to_int and is_int of the SMT-LIB theory Reals_Ints. Notice that the support is only avalaible through the Dolmen frontend.

Example

For instance, the input file input.smt2:

(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`

Model Generation

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 answers: sat, unsat or unknown.

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 Github repository.

Usage

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 --use-fpa and --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.

Usage

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 new bvnot primitive that slipped through the cracks. The bug was found immediately after the release, and version 2.5.1 released with a fix.

Acknowledgements

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.

---

About Alt-Ergo

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 Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.

This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.