Missing a case for inhaling (quantified wand with predicates on both sides)

[viper-admin]

Created by @alexanderjsummers on 2020-01-02 00:26

(forall i: Int :: i == 0 ==> acc(P(), write) --* acc(Q(0), write))

doesn’t have a case for inhaling:

[info]   java.lang.RuntimeException: missing translation for inhaling of (forall i: Int :: i == 0 ==> acc(P(), write) --* acc(Q(0), write))
[info]   at scala.sys.package$.error(package.scala:26)
[info]   at viper.carbon.modules.impls.DefaultInhaleModule.inhaleConnective(DefaultInhaleModule.scala:89)
[info]   at viper.carbon.modules.impls.DefaultInhaleModule.$anonfun$inhale$1(DefaultInhaleModule.scala:40)
[info]   at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:233)
[info]   at scala.collection.immutable.List.foreach(List.scala:388)
[info]   at scala.collection.TraversableLike.map(TraversableLike.scala:233)
[info]   at scala.collection.TraversableLike.map$(TraversableLike.scala:226)
[info]   at scala.collection.immutable.List.map(List.scala:294)
[info]   at viper.carbon.modules.impls.DefaultInhaleModule.inhale(DefaultInhaleModule.scala:40)
[info]   at viper.carbon.modules.impls.DefaultExpModule.checkDefinednessOfSpecAndInhale(DefaultExpModule.scala:511)

see all/issues//silicon//0388.vpr

‌