Incorrect encoding of relational predicates

[marcoeilers]

The following program does not verify (found by @jcp19):

field val: Int
field child: Ref

predicate InvLow(n: Ref) {
    acc(n.val) && acc(n.child) &&
    low(n.val) &&
    (n.child != null ==> InvLow(n.child))
}

method foldBug(tree: Ref)
    requires tree != null ==> InvLow(tree)
    ensures  tree != null ==> InvLow(tree)
{
    if (tree != null) {
        unfold InvLow(tree)
        fold InvLow(tree)
    }
}

The precondition is encoded incorrectly:

requires (p1 ==> tree != null ==> acc(InvLow(tree), write)) &&
    (p2 ==> tree_0 != null ==> acc(InvLow_0(tree_0), write)) &&
    ((p1 ==> tree != null) && (p2 ==> tree_0 != null) ==>
    InvLow$_low(tree, tree_0))

This is not well-defined; the InvLow$_low function should only be called when p1 and p2 are true.

[jcp19]

the credit for this finding goes to @AkasakaJelos.