blob: 146ba445c12f50c64b15a034e56e852d97e52953 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %boogie /proverWarnings:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function Map#Domain<QUN, YAN>(Map QUN YAN): [QUN] bool;
function Map#Empty<QUN, YAN>(): Map QUN YAN;
type Map QUN YAN;
axiom (forall<QUN, YAN> u: QUN ::
{ Map#Domain(Map#Empty(): Map QUN YAN)[u] }
!Map#Domain(Map#Empty(): Map QUN YAN)[u]);
procedure P()
{
}
|