Test/datatypes/ex.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13

// RUN: %boogie -typeEncoding:m %s > %t
// RUN: %diff %s.expect %t
type{:datatype} finite_map;
function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;

type{:datatype} partition;
function{:constructor} partition(owners:[int]int, vars:[int]finite_map):partition;

procedure P(arr:finite_map)
  requires dom#finite_map(arr)[0];
  ensures  dom#finite_map(arr)[0];
{
}