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