Test/z3api/boog29.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

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(false);
assert (c==0);

c := LIFT(true);
assert (c!=0);
/*
c := LIFT(1==5);
assert (c==0);
*/
}