blob: e9a785741b9b0a742a226cadf4e86d2504e4715b (
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
28
29
30
|
// 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 Box, C;
function box<a>(a) returns (Box);
function unbox<a>(Box) returns (a);
axiom (forall<a> x:a :: unbox(box(x)) == x);
axiom (forall<a> x:Box :: {unbox(x):a} box(unbox(x):a) == x);
axiom (forall x:Box :: box(unbox(x)) == x); // warning
procedure P() {
var b : Box;
var i : C;
assert unbox(box(13)) == 13;
i := unbox(b);
assert b == box(i);
assert false;
}
|
