blob: 9177e2ca1ebb0b9a0a61323a4413c889867779c5 (
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;
}
|
