blob: 4757b5b9499d37c6d85226b6f7a3214d6509f069 (
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;
}
|
