--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] What is the point of ``All models'' in Alt-Ergo?



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