Trywhy3 nontermination
On the following code (with the invariant 0 <= q commented out), TryWhy3 seems to not terminate when it should simply exhaust its number of steps and fail.
I tried to reduce the default max number of steps to 50 and it did terminate, but it took more than 30 seconds. The default is 100 steps, and I gave up on it after several minutes.
(* Russian peasant multiplication *)
use int.Int
use ref.Ref
use int.EuclideanDivision
let product (a b: int): int
requires { 0 <= b }
ensures { result = a*b }
=
let p = ref a in
let q = ref b in
let r = ref 0 in
while !q > 0 do
invariant { !p * !q + !r = a * b }
(*invariant { 0 <= !q }*)
variant { !q }
if mod !q 2 = 1 then r := !r + !p;
p := !p + !p;
q := div !q 2
done;
!r