blob: a619968ee6266f7508864183d5c4b03d3289155f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t
// RUN: %diff %s.expect %t
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }
var {:linear ""} g:int;
procedure A()
{
}
procedure B()
{
call A();
assert false;
}
|
