Test/z3api/Boog24.bpl


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

type ref;
 
function LIFT(a:bool) returns (int);
axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);

procedure  main ( ) 

{
var a : int;
var b : int;
var c : int;

c := LIFT (b < a) ;
assert (c != 0 <==> b < a);

}