--- layout: fc_discuss_archives title: Message 15 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?



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