--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on December 2014 ---
Hello, Le 2014-12-30 13:01, Mohamed Iguernelala a ?crit : > I'm pleased to announce a new public release of Alt-Ergo (version 0.99.1). For those like me wondering about the main changes, here there are (found at http://alt-ergo.ocamlpro.com/download.php): * the "SAT solving" part can now be delegated to an external plugin; * new experimental SAT solver based on mini-SAT, provided as a plugin. This solver is, in general, more efficient on ground problems; * heuristics simplification in the default SAT solver and in the matching (instantiation) module; * re-implementation of internal literals representation; * improvement of theories combination architecture; * rewriting some parts of the formulas module; * bugfixes in records and numbers modules; * new option "-no-Ematching" to perform matching without equality reasoning (i.e. without considering "equivalence classes"). This option is very useful for benchmarks coming from Atelier-B; * two new experimental options: "-save-used-context" and "-replay-used-context". When the goal is proved valid, the first option allows to save the names of useful axioms into a ".used" file. The second one is used to replay the proof using only the axioms listed in the corresponding ".used" file. Note that the replay may fail because of the absence of necessary ground terms generated by useless axioms (that are not included in .used file) during the initial run. Best regards, david