Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] Release of Alt-Ergo 0.99.1

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