blob: e7a0e6944891e17ad110225f671e5b26cd3f43ab (
plain)
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];
{
}
|
