Commit 4dfa48b8 authored by David Hauzar's avatar David Hauzar

Reformatting of counterexample example.

parent 35dcc6d9
......@@ -22,7 +22,11 @@ module M
ensures { !x < old !x }
=
incr x;
while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
while "model" "model_trace:cond" !x > 0 do
invariant { !x >= 0 }
variant { !x }
x := !x - 1
done
(**************************************
** Getting counterexamples for maps **
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment