quantified permissions on the right of a magic wand cause stack trace

[alexanderjsummers]

Using quantified permissions on the left of a wand seems OK, but on the RHS I get a stack trace. For example, for the program:

field val : Int

method foo(x:Set[Ref]) {
    package true --* forall r:Ref :: r != null ==> acc(r.val)
}

I get the following (slightly abridged):

Exception in thread "main" java.lang.RuntimeException: impure expression not caught in exhaleExt
at scala.sys.package$.error(package.scala:27)
at viper.carbon.modules.impls.DefaultWandModule.exhaleExtExp(DefaultWandModule.scala:339)
at viper.carbon.modules.impls.DefaultWandModule.exhaleExt(DefaultWandModule.scala:329)
at viper.carbon.modules.impls.DefaultWandModule.exhaleExt(DefaultWandModule.scala:320)
at viper.carbon.modules.impls.DefaultWandModule.exhaleExt(DefaultWandModule.scala:320)
at viper.carbon.modules.impls.DefaultWandModule.exec(DefaultWandModule.scala:309)
at viper.carbon.modules.impls.DefaultWandModule.translatePackageBody(DefaultWandModule.scala:259)
at viper.carbon.modules.impls.DefaultWandModule.translatePackage(DefaultWandModule.scala:238)
at viper.carbon.modules.impls.DefaultStmtModule.simpleHandleStmt(DefaultStmtModule.scala:223)
at viper.carbon.modules.impls.DefaultStmtModule.handleStmt(DefaultStmtModule.scala:94)
at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$5(DefaultStmtModule.scala:267)
at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$5$adapted(DefaultStmtModule.scala:264)
at scala.collection.immutable.List.foreach(List.scala:333)
at viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:264)
at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$3(DefaultStmtModule.scala:252)
at scala.collection.immutable.List.map(List.scala:246)
at scala.collection.immutable.List.map(List.scala:79)
at viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:252)
at viper.carbon.modules.impls.DefaultStmtModule.$anonfun$translateStmt$3(DefaultStmtModule.scala:252)
at scala.collection.immutable.List.map(List.scala:246)
at scala.collection.immutable.List.map(List.scala:79)
at viper.carbon.modules.impls.DefaultStmtModule.translateStmt(DefaultStmtModule.scala:252)
at viper.carbon.modules.impls.DefaultMainModule.translateMethodDecl(DefaultMainModule.scala:148)
at viper.carbon.modules.impls.DefaultMainModule.$anonfun$translate$9(DefaultMainModule.scala:100)
at scala.collection.immutable.List.flatMap(List.scala:293)
at scala.collection.immutable.List.flatMap(List.scala:79)
at viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:100)
....