Test/z3api/boog4.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

type ref;
type Wicket;

const w: Wicket;
const myBool: bool;
const v: Wicket;

var favorite: Wicket;

function age(Wicket) returns (int);

axiom age(w)==7;
axiom 7 < 8;
axiom 7 <= 8;

axiom 8 > 7;
axiom 8 >= 7;
axiom 6 != 7;
axiom 7+1==8;
axiom 8-1==7;
axiom 7/1==7;
axiom 7%2==1;
axiom 4*2==8;
axiom ((7==7) || (8==8));
axiom ((7==7) ==> (7<8));
axiom ((7==7) <==> (10==10));
axiom ((7==7) && (8==8));

axiom 7!=7;


procedure NewFavorite(p: Wicket);
  modifies favorite
;

  ensures favorite==p;

implementation NewFavorite(l: Wicket) {
  favorite:=l;
}