Predicate trigger in existential leads to exception
marcoeilers opened this issue · 0 comments
marcoeilers commented
The following program leads to an exception:
predicate P(x: Int)
method m(r: Int)
requires P(r)
{
//assume forall x: Int :: { P(x) } perm(P(x)) > none ==> x > 2
assume exists x: Int :: { P(x) } perm(P(x)) > none
}
which complains
Caused by: java.lang.RuntimeException: I did not expect non-quantified chunks on the heap for resource P, but found P($t@2@16; r@1@16) # W
at scala.sys.package$.error(package.scala:27)
at viper.silicon.rules.quantifiedChunkSupporter$.$anonfun$splitHeap$1(QuantifiedChunkSupport.scala:312)
at viper.silicon.rules.quantifiedChunkSupporter$.$anonfun$splitHeap$1$adapted(QuantifiedChunkSupport.scala:306)
at scala.collection.immutable.Vector.foreach(Vector.scala:1856)
at viper.silicon.rules.quantifiedChunkSupporter$.splitHeap(QuantifiedChunkSupport.scala:306)
at viper.silicon.rules.evaluator$.generatePredicateTrigger(Evaluator.scala:1455)
The exception does not occur if the commented-out assumption of the universal quantifier is uncommented.