Fixing issues #410 and #338

src/main/scala/rules/ChunkSupporter.scala

@@ -256,7 +256,12 @@ object chunkSupporter extends ChunkSupportRules {
       case Some(ch) if v.decider.check(IsPositive(ch.perm), Verifier.config.checkTimeout()) =>
         Q(s, ch.snap, v)
       case _ if v.decider.checkSmoke(true) =>
-        Success() // TODO: Mark branch as dead?
+        if (s.isInPackage) {
+          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
+          Q(s, snap, v)
+        } else {
+          Success() // TODO: Mark branch as dead?
+        }
       case _ =>
         createFailure(ve, v, s, "looking up chunk", true)
     }

src/main/scala/rules/Executor.scala

@@ -494,7 +494,7 @@ object executor extends ExecutionRules {
         consume(s, a, false, pve, v)((s1, _, v1) =>
           Q(s1, v1))
 
-      case assert @ ast.Assert(a: ast.FalseLit) =>
+      case assert @ ast.Assert(a: ast.FalseLit) if !s.isInPackage =>
         /* "assert false" triggers a smoke check. If successful, we backtrack. */
         executionFlowController.tryOrFail0(s.copy(h = magicWandSupporter.getEvalHeap(s)), v)((s1, v1, QS) => {
           if (v1.decider.checkSmoke(true))
@@ -653,7 +653,7 @@ object executor extends ExecutionRules {
 
       case pckg @ ast.Package(wand, proofScript) =>
         val pve = PackageFailed(pckg)
-          magicWandSupporter.packageWand(s, wand, proofScript, pve, v)((s1, chWand, v1) => {
+          magicWandSupporter.packageWand(s.copy(isInPackage = true), wand, proofScript, pve, v)((s1, chWand, v1) => {
 
             val hOps = s1.reserveHeaps.head + chWand
             assert(s.exhaleExt || s1.reserveHeaps.length == 1)
@@ -692,7 +692,7 @@ object executor extends ExecutionRules {
               case _ => s2.smCache
             }
 
-            continuation(s2.copy(smCache = smCache3), v1)
+            continuation(s2.copy(smCache = smCache3, isInPackage = s.isInPackage), v1)
           })
 
       case apply @ ast.Apply(e) =>

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -19,7 +19,7 @@ import viper.silicon.utils.ast.{BigAnd, buildMinExp, removeKnownToBeTrueExp, rep
 import viper.silicon.verifier.Verifier
 import viper.silicon.{MList, MMap}
 import viper.silver.ast
-import viper.silver.parser.{PKw, PPrimitiv, PReserved}
+import viper.silver.parser.PUnknown
 import viper.silver.verifier.VerificationError
 
 import scala.collection.mutable.ListBuffer
@@ -204,7 +204,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
 
     if (relevantChunks.isEmpty) {
       if (v.decider.checkSmoke(true)) {
-        Success() // TODO: Mark branch as dead?
+        if (s.isInPackage) {
+          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
+          Q(s, snap, v)
+        } else {
+          Success() // TODO: Mark branch as dead?
+        }
       } else {
         createFailure(ve, v, s, False, "branch is dead")
       }

src/main/scala/rules/Producer.scala

@@ -323,7 +323,7 @@ object producer extends ProductionRules {
           eval(s1, perm, pve, v1)((s2, tPerm, ePermNew, v2) =>
             permissionSupporter.assertNotNegative(s2, tPerm, perm, ePermNew, pve, v2)((s2a, v3) => {
               val s3 = s2a.copy(constrainableARPs = s.constrainableARPs)
-              val snap = sf(v3.symbolConverter.toSort(field.typ), v3)
+              val snap = sf(v3.snapshotSupporter.optimalSnapshotSort(field, s3, v3), v3)
               val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(field))
                 PermTimes(tPerm, s3.permissionScalingFactor)
               else
@@ -350,9 +350,7 @@ object producer extends ProductionRules {
           eval(s1, perm, pve, v1)((s1a, tPerm, ePermNew, v1a) =>
             permissionSupporter.assertNotNegative(s1a, tPerm, perm, ePermNew, pve, v1a)((s1b, v2) => {
               val s2 = s1b.copy(constrainableARPs = s.constrainableARPs)
-              val snap = sf(
-                predicate.body.map(v2.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
-                              .getOrElse(sorts.Snap), v2)
+              val snap = sf(v2.snapshotSupporter.optimalSnapshotSort(predicate, s2, v2), v2)
               val gain = if (!Verifier.config.unsafeWildcardOptimization() || s2.permLocations.contains(predicate))
                 PermTimes(tPerm, s2.permissionScalingFactor)
               else
@@ -382,7 +380,7 @@ object producer extends ProductionRules {
         val formalVarExps = Option.when(withExp)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)()))
         evals(s, bodyVars, _ => pve, v)((s1, args, bodyVarsNew, v1) => {
           val (sm, smValueDef) =
-            quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(sorts.Snap, v1), v1)
+            quantifiedChunkSupporter.singletonSnapshotMap(s1, wand, args, sf(v1.snapshotSupporter.optimalSnapshotSort(wand, s1, v1), v1), v1)
           v1.decider.prover.comment("Definitional axioms for singleton-SM's value")
           val definitionalAxiomMark = v1.decider.setPathConditionMark()
           val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true))
@@ -416,7 +414,7 @@ object producer extends ProductionRules {
           Q(s2, v1)})
 
       case wand: ast.MagicWand =>
-        val snap = sf(sorts.MagicWandSnapFunction, v)
+        val snap = sf(v.snapshotSupporter.optimalSnapshotSort(wand, s, v), v)
         magicWandSupporter.createChunk(s, wand, MagicWandSnapshot(snap), pve, v)((s1, chWand, v1) =>
           chunkSupporter.produce(s1, s1.h, chWand, v1)((s2, h2, v2) =>
             Q(s2.copy(h = h2), v2)))
@@ -431,7 +429,7 @@ object producer extends ProductionRules {
           else Some(forall.triggers)
         evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) {
           case (s1, qvars, qvarExps, Seq(tCond), eCondNew, Some((Seq(tRcvr, tPerm), rcvrPerm, tTriggers, (auxGlobals, auxNonGlobals), auxExps)), v1) =>
-            val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1)
+            val tSnap = sf(sorts.FieldValueFunction(v1.snapshotSupporter.optimalSnapshotSort(acc.loc.field, s1, v1), acc.loc.field.name), v1)
             val s1a = s1.copy(constrainableARPs = s.constrainableARPs)
             quantifiedChunkSupporter.produce(
               s1a,

src/main/scala/state/State.scala

@@ -62,6 +62,7 @@ final case class State(g: Store = Store(),
                        conservedPcs: Stack[Vector[RecordedPathConditions]] = Stack(),
                        recordPcs: Boolean = false,
                        exhaleExt: Boolean = false,
+                       isInPackage: Boolean = false,
 
                        ssCache: SsCache = Map.empty,
                        assertReadAccessOnly: Boolean = false,
@@ -175,7 +176,7 @@ object State {
                  triggerExp1,
                  partiallyConsumedHeap1,
                  permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld,
-                 reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
+                 reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, isInPackage1,
                  ssCache1, assertReadAccessOnly1,
                  qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1,
                  predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
@@ -200,7 +201,7 @@ object State {
                      triggerExp2,
                      `partiallyConsumedHeap1`,
                      `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`,
-                     `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
+                     `reserveHeaps1`, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, `isInPackage1`,
                      ssCache2, `assertReadAccessOnly1`,
                      `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, `smDomainNeeded1`,
                      `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
@@ -331,7 +332,7 @@ object State {
       triggerExp1,
       partiallyConsumedHeap1,
       permissionScalingFactor1, permissionScalingFactorExp1, isEvalInOld,
-      reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1,
+      reserveHeaps1, reserveCfgs1, conservedPcs1, recordPcs1, exhaleExt1, isInPackage1,
       ssCache1, assertReadAccessOnly1,
       qpFields1, qpPredicates1, qpMagicWands1, permResources1, smCache1, pmCache1, smDomainNeeded1,
       predicateSnapMap1, predicateFormalVarMap1, retryLevel, useHeapTriggers,
@@ -355,7 +356,7 @@ object State {
           triggerExp2,
           partiallyConsumedHeap2,
           `permissionScalingFactor1`, `permissionScalingFactorExp1`, `isEvalInOld`,
-          reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`,
+          reserveHeaps2, `reserveCfgs1`, conservedPcs2, `recordPcs1`, `exhaleExt1`, `isInPackage1`,
           ssCache2, `assertReadAccessOnly1`,
           `qpFields1`, `qpPredicates1`, `qpMagicWands1`, `permResources1`, smCache2, pmCache2, smDomainNeeded2,
           `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,

src/main/scala/supporters/SnapshotSupporter.scala

@@ -8,17 +8,20 @@ package viper.silicon.supporters
 
 import viper.silicon.debugger.DebugExp
 import viper.silicon.state.terms.{Combine, First, Second, Sort, Term, Unit, sorts}
-import viper.silicon.state.{State, SymbolConverter}
+import viper.silicon.state.{MagicWandIdentifier, State, SymbolConverter}
 import viper.silicon.utils.toSf
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
+import viper.silver.ast.Resource
 import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion
 
 import scala.annotation.unused
 
 trait SnapshotSupporter {
   def optimalSnapshotSort(a: ast.Exp, program: ast.Program): (Sort, Boolean)
 
+  def optimalSnapshotSort(r: ast.Resource, s: State, v: Verifier): Sort
+
   def createSnapshotPair(s: State,
                          sf: (Sort, Verifier) => Term,
                          a0: ast.Exp,
@@ -31,6 +34,17 @@ class DefaultSnapshotSupporter(symbolConverter: SymbolConverter) extends Snapsho
   def optimalSnapshotSort(a: ast.Exp, program: ast.Program): (Sort, Boolean) =
     optimalSnapshotSort(a, program, Nil)
 
+  def optimalSnapshotSort(r: Resource, s: State, v: Verifier): Sort = r match {
+    case f: ast.Field => v.symbolConverter.toSort(f.typ)
+    case p: ast.Predicate if s.predicateSnapMap.contains(p) => s.predicateSnapMap(p)
+    case p: ast.Predicate =>
+      p.body.map(v.snapshotSupporter.optimalSnapshotSort(_, s.program)._1)
+        .getOrElse(sorts.Snap)
+    case mw: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(mw, s.program)) =>
+      sorts.Snap
+    case _: ast.MagicWand => sorts.MagicWandSnapFunction
+  }
+
   private def optimalSnapshotSort(a: ast.Exp, program: ast.Program, visited: Seq[String])
                                  : (Sort, Boolean) =