Chalice/tests/regressions/internal-bug-7.chalice


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

class Node {
  var n: Node
  
  predicate P { acc(n) && (n != null ==> acc(n.P)) }

  function length(): int
    requires rd(P)
    ensures result >= 1
  { unfolding rd(P) in 1 + (n == null ? 0 : n.length()) }
  
}

class Test {
  method test(node: Node)
    requires node != null
    requires acc(node.P)
  {
    assert node.length() >= 1
    assert (unfolding rd(node.P) in node.n == null) ==> (node.length() == 1) /* Holds in Chalice and Syxc */
    //assert (unfolding rd(node.P) in node.n != null) ==> (unfolding rd(node.P) in node.n.length() >= 1) /* Holds in Chalice and Syxc */
    assert (unfolding rd(node.P) in node.n != null) ==> (node.length() > 1) /* Holds in Chalice and Syxc */
    assert (node.length() == 1) ==> (unfolding rd(node.P) in node.n == null) /* Fails in Chalice and Syxc */
    assert (node.length() == 1) <==> (unfolding rd(node.P) in node.n == null)
    // assert n.length() > 1 <==> unfolding rd(n.P) in n.n != null /* Fails in Chalice and Syxc */
  }
}