Test/z3api/boog11.bpl


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

type ref;
// types
const top: ref;
var myRef: ref;

// procedure
procedure SetTo(r: ref);
  modifies myRef
;

  ensures myRef==r;

implementation SetTo(c: ref) {
  myRef:=top;
}