[Boogie] Cannot verify datatype values

Feb 11, 2013 at 8:02 PM
Edited Feb 11, 2013 at 8:06 PM
I would like to know why the boogie code ( http://rise4fun.com/Boogie/QOa ) 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);

class Node{
    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)
}

Thanks
Yuyan