Dear Why3 Club,
I have a why3 script that I think is relatively simple but why3 cannot
prove it. I wander if I did anything wrong.
*constant X : (map int int)*
*context:
*
* X[4] = X[6] && X[5] = X[6] && X[6] < X[7]
*
*predicate:
*
* exists k : int. 0 <= k && k <= 3 && not(X[k+4] = X[k+5])*
It is obvious that there exists such a k = 2. If I modify the predicate a
lilltle bit to :
*predicate:
*
* exists k : int. 0 <= k && k <= 3 && k = 2 && not(X[k+4] = X[k+5])*
why3 then has no problem to prove it. So I'm confused that why why3 cannot
prove the original case.
Thanks,
Ziqing Luo
University of Delaware
The following is the whole why3 script:
theory Why3Query_408
use import int.Int
use import map.Map
constant _X : (map int int)
(*
context:
X[4] = X[6]
X[5] = X[6]
X[6] < X[7]
predicate:
exists k : int. 0 <= k && k <= 3 && not(X[k+4] = X[k+5])
*)
predicate context = (((0) = ((get _X (4)) + ((-1) * (get _X (6)))))
&&
((0) = ((get _X (5)) + ((-1) * (get _X (6))))) &&
(((get _X (6)) + ((-1) * (get _X (7))) + (1))
<= (0)))
goal G0: context -> ((exists k : int. (((k + (-3)) <= (0)) && ((0)
<= k) &&
(not ((0) = ((get _X (k + (4))) + ((-1) *
(get _X (k + (5))))))))) )
end
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
