Test all/assume/assume10QPwand.sil causes Boogie errors

[viper-admin]

Created by @mschwerhoff on 2018-10-11 15:55
Last updated on 2019-07-27 02:34

java.lang.RuntimeException: missing translation for inhaling of (forall x: Ref, y: Ref, z: Ref :: { (x in xs),(y in ys),(z in zs) } (x in xs) && ((y in ys) && (z in zs)) ==> acc(x.f, write) && (acc(y.f, write) && acc(z.f, write)) --* acc(p(x, y, z), write))
   at scala.sys.package$.error(package.scala:27)
   at viper.carbon.modules.impls.DefaultInhaleModule.viper$carbon$modules$impls$DefaultInhaleModule$$inhaleConnective(DefaultInhaleModule.scala:74)
   at viper.carbon.modules.impls.DefaultInhaleModule$$anonfun$inhale$1.apply(DefaultInhaleModule.scala:33)
   at viper.carbon.modules.impls.DefaultInhaleModule$$anonfun$inhale$1.apply(DefaultInhaleModule.scala:33)
   at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
   at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
   at scala.collection.immutable.List.foreach(List.scala:381)
   at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
   at scala.collection.immutable.List.map(List.scala:285)
   at viper.carbon.modules.impls.DefaultInhaleModule.inhale(DefaultInhaleModule.scala:33)
   ...

[viper-admin]

@alexanderjsummers commented on 2018-10-11 15:58

This is a missing case in Carbon's translation

[viper-admin]

@alexanderjsummers commented on 2018-10-11 15:58

Duplicate of #205.

[viper-admin]

@alexanderjsummers on 2018-10-11 15:58:

• changed state from new to duplicate

[viper-admin]

@mschwerhoff on 2018-10-12 13:30:

• edited the title

[viper-admin]

@marcoeilers commented on 2019-07-27 02:34

Not a duplicate of #205, I'm pretty sure the issue here is the magic wand inside a quantifier, not the multiple quantified variables.

[viper-admin]

@marcoeilers on 2019-07-27 02:34:

• changed state from duplicate to open

[fpoli]

Indeed, Carbon doesn't seem to support quantified magic wands. I get the same kind of Java exception with the following program.

predicate P(x: Int)

method lemma()
    requires forall x: Int :: P(x) --* P(x)