blob: 876d879de58b1f6361741a6617dc1e6e4da5d799 (
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
|
// RUN: %boogie -typeEncoding:m "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
type TT;
type {:datatype} Tree;
function {:constructor} leaf() : Tree;
function {:constructor} node(value:TT, children:TreeList) : Tree;
type {:datatype} TreeList;
function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;
function {:constructor} nil() : TreeList;
procedure foo()
{
var a: Tree;
var b: TreeList;
var x: TT;
assert value#node(node(x, nil())) == x;
assert children#node(node(x, nil())) == nil();
assert (cons(leaf(), nil()) != nil());
assert is#nil(nil());
assert is#node(leaf());
}
|