Inconsistency is reported when two conditions are conjuncted in an assertion.

Mar 3, 2013 at 10:09 PM
Inconsistency is reported when two conditions (n.data == 5 and n.Valid()) are conjuncted in the assertion in a method Main. However It is fine if the two conditions are asserted separately.
class Node<T> {
  var list: seq<T>;
  var footprint: set<Node<T>>;

  var data: T;
  var next: Node<T>;

  function Valid(): bool
    reads this, footprint;
  {
    this in this.footprint && null !in this.footprint &&
    (next == null ==> list == [data]) &&
    (next != null ==>
        next in footprint && next.footprint <= footprint &&
        this !in next.footprint &&
        list == [data] + next.list &&
        next.Valid())
  }

  method Init(d: T)
    modifies this;
    ensures Valid() && fresh(footprint - {this});
    ensures list == [d];
    ensures data == d;
  {
    data := d;
    next := null;
    list := [d];
    footprint := {this};
  }

 method Main()
  {
    var n :=  new Node<int>.Init(5);
    //assert n.data == 5;
    //assert n.Valid();
    assert n.data == 5 && n.Valid(); // inconsistency occurs
  }
}
Thanks
Yuyan
Mar 23, 2013 at 12:01 AM
In fact, I do not know why this happens, but I am very interested in this issue..

Nightrise