blob: 0287da1230fa2d8aa1f859710714ddd24f1e4781 (
plain)
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
|
// RUN: %boogie -noinfer -typeEncoding:m "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type TT;
procedure A()
{
var M : [int]bool;
var N : [int,int]bool;
var Z : [int,bool]TT;
var t : TT;
M[10] := true;
M[20] := false;
N[10,20] := true;
N[10,21] := false;
N[11,20] := false;
assert M[10];
assert !M[20];
assert N[10,20];
assert !N[11,20];
assert !N[10,21];
assert Z[10,true] == t;
}
|