summaryrefslogtreecommitdiff
path: root/Test/z3api/boog11.bpl
blob: 5b83de6ace7f8d6e60d5d986b0dcab294379f5c3 (plain)
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;
}