[Why3-club] Is this goal really (un)tractable ?
Jean-Christophe.Filliatre at lri.fr
Thu Feb 23 09:50:55 CET 2012
On 22/02/2012 16:48, Jean-Christophe Filliatre wrote:
> On my machine, using the git version of Why3, your goal is proved in no
> time (under 0.04s) by Alt-ergo 0.94, CVC3 2.2, Yices 1.0.25, and Z3 2.19.
Oups, I took another goal by accident; my mistake.
With the right one, only Z3 (2.19) proves it.
I attach the input file for Alt-ergo on that goal. The issue is axiom
"value_inversion". Alt-ergo finds no appropriate trigger for it, so it
simply discards it. Therefore it gives up immediately.
If you manually give "u" as a trigger for this axiom, that is
axiom value_inversion :
(forall u:value [u].
((u = Int(Int_proj_1(u))) or (u = Loc(Loc_proj_1(u)))))
then Alt-ergo easily proves it. I've CC'ed Sylvain.
Such an axiom is generated automatically by Why3, to encode the
algebraic data type "value". So we should do something to add such a
Regarding Z3, CVC3, and Yices, it is more tricky, since we don't pass
them triggers (and we don't even have a way to do it in some cases). As
you see, Z3 is able to use the axiom anyway, but CVC3 and Yices don't.
-------------- section suivante --------------
Un texte encapsul? et encod? dans un jeu de caract?res inconnu a ?t? nettoy?...
Nom : test-T-eval_case.why
URL : <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20120223/c94a4802/attachment.txt>
More information about the Why3-club