hyperGobra: incorrect encoding of forall with --hyperMode=on

[henriman]

I am working on verifying SIF for the VerifiedSCION router (using hyperGobra) with @jcp19.

requires low(b)
func test1(b [2]int) {
    assert low(b[0])
    assert low(b[1])
    // Fails:
    assert forall i int :: { b[i] } 0 <= i && i < 2 ==> low(b[i])
}

Trying to verify the above code using --hyperMode=on fails in asserting the last assertion.

The problem: During the product-program construction, i is also duplicated (or: the duplicated i are not related to each other):

assert (forall i_V10: Int, i_V11: Int ::
    { unbox_Emb_2_Intint$$$$_E_$$$_Seq_Int(b_V0_CN00)[i_V10], unbox_Emb_2_Intint$$$$_E_$$$_Seq_Int(b_V0_CN01)[i_V11] }
    0 <= i_V10 && i_V10 < 2 && (0 <= i_V11 && i_V11 < 2) ==>
    unbox_Emb_2_Intint$$$$_E_$$$_Seq_Int(b_V0_CN00)[i_V10] ==
    unbox_Emb_2_Intint$$$$_E_$$$_Seq_Int(b_V0_CN01)[i_V11])

This could be fixed either by inserting i_V10 == i_V11 ==> after ==>, or by not duplicating i (which is not necessary to do, from my understanding).

Using --hyperMode=extended, the code verifies successfully.