Test/test2/TypeEncodingM.bpl


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;
}