blob: d26c617c7fb238740a8bfb233835cf719f6090f4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
procedure main ( )
{
var c: int;
c := LIFT(1==5);
assert (c==0);
}
|