A new release of Alt-Ergo (version 2.4.0) is available.
You can get it from Alt-Ergo’s website. The associated opam package will be published in the next few days.
This release contains some major novelties:
- Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
- We switched command line parsing to use cmdliner. You will need to use
--<option name>instead of
-<option name>. Some options have also been renamed, see the manpage or the documentation.
- We improved the online documentation of your solver, available here.
This release also contains some minor novelties:
.whyextension are depreciated, the use of
.aeextension is advised.
--output) option to manually set the input (resp output) file format
--pretty-outputoption to add better debug formatting and to add colors
- Add exponentiation operation,
**in native Alt-Ergo syntax. The operator is fully interpreted when applied to constants
--steps-countand improve the way steps are counted (AdaCore contribution)
--instantiation-heuristicoption that can enable lighter or heavier instantiation
- Reduce the instantiation context (considered foralls / exists) in CDCL-Tableaux to better mimic the Tableaux-like SAT solver
- Multiple bugfixes
The full list of changes is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!
OCamlPro SAS is an INRIA spin-off company created in April 2011 to promote the use of the OCaml programming language in the industrial sector. It actively participates in research and development aimed at improving safety and security in the security of computer applications in general. You will find more information on our website: http://www.ocamlpro.com.