Test/z3api/boog12.bpl


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

type ref;
// types
type Color;
const blue: Color;

var myArray:[int] Color;
var myMatrix:[int,int] Color;

// procedure
procedure SetTo(c: Color);
  modifies myArray, myMatrix
;

  ensures myArray[0]==c;

implementation SetTo(c: Color) {
  myMatrix[0,1]:=c;
  myArray[0]:=blue;
}