blob: 8a1bc803d5d470dbb416a1b6d2fcd2b70e69d31b (
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;
}
|