--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2016 ---
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