blob: 3b9bccf2812da4148f7703c15db19de16b452037 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
// RUN: %diff %s.n.expect %t
// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
// RUN: %diff %s.p.expect %t
// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
// RUN: %diff %s.a.expect %t
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
}
|