viperproject/silicon

Predicate trigger in existential leads to exception

marcoeilers opened this issue · 0 comments

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.