blob: 3633e704b46e417323fb99ae09267188702c7ded (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
function f<a>(a) returns (bool);
function g(int) returns (bool);
axiom (forall x:int :: f(x));
axiom (forall x:int :: g(x));
procedure P() returns () {
var x : int, m : [int]int;
assert f(x);
assert f(m[x]);
assert g(x);
assert g(m[x]);
assert f(true); // should not be provable
}
|
