QP single-recvr merge Issue

[mlimbeck]

Currently, we merge QP single-receiver chunks if they have the same singletonArguments. This implicitly assumes that their conditions are also identical. However, this assumption does not hold when chunks with the same receiver originate from separate branches and are joined using moreJoins. In such cases, additional conjuncts may have been added to the conditions. Therefore, we need to verify that both the conditions and the receivers match before merging the chunks.
The following example illustrates this issue more clearly:

field f: Int

// issue when run with --moreJoins 2
method foo(x: Ref, xs: Set[Ref])
    requires acc(x.f, 1/2)
    requires forall r: Ref :: { r in xs } r in xs ==> acc(r.f)
{
    var b: Bool

    if (b) {
        inhale acc(x.f, 1/2)
        // At this point, there are two separate single-receiver-qp-chunks:
        // 1) forall r: Ref :: (r == x ? 1/2 : Z)
        // 2) forall r: Ref :: (r == x ? 1/2 : Z)
        // These chunks are merged into a single combined chunk:
        //    `forall r: Ref :: (r == x ? W : Z)`
    } else {
        inhale acc(x.f, 1/2)
        // same here
    }

    assert acc(x.f)
    // After joining the two branches, we again have two chunks:
    // 1) forall r: Ref :: (b && r == x ? W : Z)
    // 2) forall r: Ref :: (!b && r == x ? W : Z)
    // The qp-merging logic assumes all chunks for the same receiver x share the same condition.
    // This assumption breaks because the conditions differ between the branches.
    // As a result, the chunks are merged by retaining the condition of the first chunk
    // and summing their permissions:
    //    (b && r == x ? 2/1 : Z)
}

Q: Should we add this example as a test case? If so, where should be add it?

Fixes: #883

[marcoeilers]

Thanks a lot!
I think it's best if you file an issue for this, since you already have a minimized example that shows the problem, and then add the test in the silver repository as the test for that issue.