Unrelated fold removes knowledge of quantifier with predicate unside

[sakehl]

The following program does not verify. Whilst if you remove fold acc(hide1(x1, n, i),1/2) from line 21, it does verify. And I believe that line 21 should be unrelated to the given verification failure:

Silicon 1.1-SNAPSHOT (ad3593f7)
Silicon found 1 error in 3.18s:
  [0] Assert might fail. Assertion (forall j: Int :: { hide0(x0, n, j) } 0 <= j && j < n ==> (unfolding acc(hide0(x0, n, j), write) in aloc(x0, j).int) == 0) might not hold. (qpreds_quant1.vpr@23.11--25.56)

File

```scala method main1(tid: Int, n: Int, x0: Array, x1: Array, i: Int) requires x0 != x1 requires alen(x0) == n && alen(x1) == n requires (forall j: Int :: { hide0(x0,n,j) } 0 <= j && j < n ==> acc(hide0(x0,n,j), write) ) requires (forall j: Int :: { hide1(x1,n,j) } 0 <= j && j < n ==> acc(hide1(x1,n,j), 1/2) ) requires (forall j: Int :: { hide0(x0,n,j) } 0 <= j && j < n ==> (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0) requires i >= 0 && i < n { assert (forall j: Int :: { hide0(x0,n,j) } 0 <= j && j < n ==> (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0) unfold acc(hide1(x1, n, i),1/2) fold acc(hide1(x1, n, i),1/2) assert (forall j: Int :: { hide0(x0,n,j) } 0 <= j && j < n ==> (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0) } ////////////////////////// Other functions domain Array { function array_loc(a: Array, i: Int): Ref function alen(a: Array): Int function loc_inv_1(loc: Ref): Array function loc_inv_2(loc: Ref): Int axiom { (forall a: Array, i: Int :: { array_loc(a, i) } loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i) } axiom { (forall a: Array :: { alen(a) } alen(a) >= 0) } } field int: Int predicate hide0(x: Array, n: Int, i: Int) { n > 0 && i >= 0 && i < n && alen(x) == n && acc(aloc(x, i).int, write) } predicate hide1(x: Array, n: Int, i: Int) { n > 0 && i >= 0 && i < n && alen(x) == n && acc(aloc(x, i).int, write) } function aloc(a: Array, i: Int): Ref requires 0 <= i requires i < alen(a) decreases ensures loc_inv_1(result) == a ensures loc_inv_2(result) == i { array_loc(a, i) } ```

[sakehl]

Additionally, if you write

assert (forall j: Int :: { aloc(x0, j) }
      0 <= j && j < n ==>
      (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)

I.e. For the trigger of the quantifier, you use the function inside the unfolding.

In this case, the quantifier does not seem to trigger at all.

Although maybe this is just not allowed and fine, was not sure about this.

[marcoeilers]

Apparently this was also fixed by PR #846 (although there are some fundamental issues here that we're essentially just working around with a bunch of caching).