Feb 11, 2013 at 8:02 PM
Edited Feb 11, 2013 at 8:06 PM
I would like to know why the boogie code (
) can verify the assertion on line 845, but cannot verify the assertion on line 847.
For your convenience, here are the snippets of the corresponding Danfy code. Note that I took out the frame checking in the boogie code.
datatype datalist = data_nil | data_cons(int, datalist);
var data: int;
var next: Node;
static predicate test3(n: Node, v: int)
n!= null ==> n.data == v
static predicate test1(n: Node, lst:datalist)
n!= null ==> lst == data_cons(n.data, data_nil)