blob: f487dcab2226b6dd3044a815df4cbb4fbd214222 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
type T;
function f() returns (int); // functions without arguments
function g() returns (T);
const c : T;
axiom (f() >= 13);
axiom (g() != c);
procedure P() returns () {
var x : int;
x := f();
assert x >= 0 && f() >= 7;
assert g() != c;
assert f() >= 20; // should not be provable
}
|
