--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on January 2016 ---
From Iguernlala Mohamed <mohamed.iguernlala at ocamlpro.com>: ====== Hi, Le 27/01/2016 04:36, Wolfram Kahl 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: As said on Alt-Ergo's website (alt-ergo.ocamlpro.com), The issues tracker is here: https://github.com/OCamlPro/alt-ergo/issues > What is the point of the ``All models'' option in Alt-Ergo? As said with the help flag (alt-ergo -h), -all-models is experimental. More precisely, it is a one-day hack we made for an intern 5 years ago. > 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)''. Because, with this option enabled, every time Alt-Ergo finds a model, it (is supposed to) (1) dump(s) it on standard output, and then (2) act as if the branch was unsat to use backtracking capabilities of the solver and search for other models. So, it is easy to detect (when the option is activated) whether the input formula is unsat (valid) or not by updating a global flag when the first model is found. Unfortunately, this was not done during the one-day hack .... and no one complained about this behavior. :-) > (Without that option, it only says ``I don't know (sat) (0.01s)'', > which I still consider as a rather weak answer...) Current versions of Alt-Ergo never try to investigate whether the input formula is invalid (sat) when they fail to prove it is valid(unsat), even on trivial formulas like "0 = 1" > 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''? By design of "all models" as said above, but it could be fixed. A workaround is to run Alt-Ergo twice on the Formula: once without the option to see if the forumula is valid, and once with the option to get models. Regards, Mohamed. -- Senior R&D Engineer, OCamlPro SAS Research Associate, VALS team, LRI Webpage: http://www.iguer.info