blob: b7a6a238b2d11505419092bdab00ef5a82ded763 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
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;
}
|
