--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on January 2016 ---
Hi, You should send your questions about Alt-Ergo to https://github.com/OCamlPro/alt-ergo/issues ; see also http://alt-ergo.ocamlpro.com/download.php L. > Le 27 janv. 2016 à 04:36, Wolfram Kahl <kahl at cas.mcmaster.ca> a écrit : > > Since I cannot find Alt-Ergo documentation nor mailing list, > I ask this question here, since I am using it only from Frama-C: > What is the point of the ``All models'' option in Alt-Ergo? > With that enabled (I am using it via the GUI as started from > WP-goals in Frama-C), it has no trouble to decide > > //@ lemma falsum: 0 == 1; > > as ``Valid (0.01s)''. > > (Without that option, it only says ``I don't know (sat) (0.01s)'', > which I still consider as a rather weak answer...) > > The closest I found to documentation is the help flag: > > alt-ergo -h > > produces > > -all-models experimental support for all models > -model experimental support for models on labeled terms > -complete-model experimental support for complete model > > , but I don't quite know how I am supposed to understand these --- > is validity of falsum a result of the experimental nature of these, > or is it by design of ``all models''? > > $ alt-ergo -version > 0.99.1 > > > Wolfram > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss