blob: 753d8801a306abc6c33bfa2cca589e8140a59089 (
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];
{
}
|