Test/z3api/boog5.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;
// types
type Wicket;

// consts
const w: Wicket;
const myBool: bool;
const v: Wicket;
const u: Wicket;
const x: Wicket;


// vars
var favorite: Wicket;

// functions
function age(Wicket) returns (int);

// axioms
axiom age(w)==6;
axiom age(u)==5;
axiom age(x)==4;


// procedure
procedure SetToSeven(p: Wicket);
  modifies favorite
;

  ensures favorite==p;

implementation SetToSeven(l: Wicket) {
  if (age(w)==7) {
    favorite:=l;
  } else {
    favorite:=v;
  }


}