Altergo2.0.0 support
Hello,
Has there been any work to support Alt-ergo2.0.0 in Why3 ? I tried to use it but why3config answered that it is not known to be supported yet.
I then tried to use it but it looks like there are bugs in the drivers. When I try to prove a lemma from examples/isqrt with it, altergo answers valid in 0.00s and the prover output is the following:
File "/tmp/why_b5dbca_isqrt-T-sqr_non_neg.why", line 17, characters 21-48:Valid (0.0000) (2 steps)
It looks like a syntax error but still says that it is valid. Is it a normal output ?
Does it possibly come from my local setup ?
PS: I am testing on branch new_ide.
File "/tmp/why_b5dbca_isqrt-T-sqr_non_neg.why":
(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
(* this is a prelude for Alt-Ergo integer arithmetic *)
logic match_bool : bool, 'a, 'a -> 'a
axiom match_bool_True :
(forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))
axiom match_bool_False :
(forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))
axiom CompatOrderMult :
(forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) ->
((x * z) <= (y * z)))))
function sqr(x: int) : int = (x * x)
goal sqr_non_neg : (forall x:int. (0 <= sqr(x)))