Asserting after assuming quantifier with heap-dependent trigger fails #959
Description
Asserting the quantifier fails, although it literally repeats the previously assumed ones. I've already done a bit of debugging, see code comments, and preliminary concluded that the heap-dependent trigger array_to_seq(...) might be the culprit.
method counting_sort(a: IArray, max: Int)
requires access(a, write)
{
var i: Int
var y: Int
assume forall k: Int :: // {k in seq_as_multiset(array_to_seq(a)[..y])} // Explicitly declaring a trigger doesn't help
// {T(k)} // The artificial trigger does the trick, though
i <= k < max ==> (k in seq_as_multiset(array_to_seq(a)[..y])) == 0
assert forall k: Int :: // 🚨🚨🚨 FAILS IN SILICON 🚨🚨🚨
i <= k < max /* && T(k) */ ==> (k in seq_as_multiset(array_to_seq(a)[..y])) == 0
}
function array_to_seq(a: IArray): Seq[Int]
requires access(a, write) // If removed, the example verifies
// requires 0 < len(a) ==> acc(loc(a, 0), write) // Causes the same problem ➜ issue unrelated to QPs?
/* ------ Debugging ------ */
domain __Debugging {
function T(k: Int): Bool
axiom { forall k: Int :: T(k) }
}
/* ------ Background theory ------ */
domain __MSHelper[T$] {
function seq_as_multiset(s: Seq[T$]): Multiset[T$]
}
field val: Int
define loc(a, i)
slot(a, i).val
define access(a, p)
forall i: Int :: {loc(a, i)}
0 <= i && i < len(a) ==> acc(loc(a, i), p)
domain IArray {
function slot(a: IArray, i: Int): Ref
function len(a: IArray): Int
function first(r: Ref): IArray
function second(r: Ref): Int
axiom all_diff {
forall a: IArray, i: Int :: {slot(a, i)}
first(slot(a, i)) == a && second(slot(a, i)) == i
}
axiom len_nonneg {
forall a: IArray :: {len(a)}
len(a) >= 0
}
}
```