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