diff --git a/silver b/silver
index 48e0ac8c6..1f4c176a7 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 48e0ac8c64a8c13581c9d9652d3b23853e7701ff
+Subproject commit 1f4c176a70d09b68a748f0e3711045c25aabdde9
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index 33362ca17..952661ef5 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -122,9 +122,9 @@ object consumer extends ConsumptionRules {
       if (tlcs.tail.isEmpty)
         wrappedConsumeTlc(s, h, a, pve, v)(Q)
       else
-        wrappedConsumeTlc(s, h, a, pve, v)((s1, h1, snap1, v1) =>
+        wrappedConsumeTlc(s, h, a, pve, v)((s1, h1, snap1, v1) => {
           consumeTlcs(s1, h1, tlcs.tail, pves.tail, v1)((s2, h2, snap2, v2) =>
-            Q(s2, h2, Combine(snap1, snap2), v2)))
+            Q(s2, h2, Combine(snap1, snap2), v2))})
     }
   }
 
@@ -234,8 +234,9 @@ object consumer extends ConsumptionRules {
         val optTrigger =
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
+
         evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.perm, acc.loc.rcv), optTrigger, qid.name, pve, v) {
-          case (s1, qvars, Seq(tCond), Seq(tPerm, tRcvr), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
+          case (s1, qvars, Seq(tCond), Some((Seq(tPerm, tRcvr), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
             quantifiedChunkSupporter.consume(
               s = s1,
               h = h,
@@ -255,6 +256,7 @@ object consumer extends ConsumptionRules {
               notInjectiveReason = QPAssertionNotInjective(acc.loc),
               insufficientPermissionReason = InsufficientPermission(acc.loc),
               v1)(Q)
+          case (s1, _, _, None, v1) => Q(s1, h, True, v1)
         }
 
       case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) =>
@@ -272,7 +274,7 @@ object consumer extends ConsumptionRules {
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
         evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid.name, pve, v) {
-          case (s1, qvars, Seq(tCond), Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
+          case (s1, qvars, Seq(tCond), Some((Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
             quantifiedChunkSupporter.consume(
               s = s1,
               h = h,
@@ -292,6 +294,7 @@ object consumer extends ConsumptionRules {
               notInjectiveReason = QPAssertionNotInjective(acc.loc),
               insufficientPermissionReason = InsufficientPermission(acc.loc),
               v1)(Q)
+          case (s1, _, _, None, v1) => Q(s1, h, True, v1)
         }
 
       case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
@@ -304,7 +307,7 @@ object consumer extends ConsumptionRules {
         val ePerm = ast.FullPerm()()
         val tPerm = FullPerm
         evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
-          case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
+          case (s1, qvars, Seq(tCond), Some((tArgs, tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
             quantifiedChunkSupporter.consume(
               s = s1,
               h = h,
@@ -324,6 +327,7 @@ object consumer extends ConsumptionRules {
               notInjectiveReason = sys.error("Quantified wand not injective"), /*ReceiverNotInjective(...)*/
               insufficientPermissionReason = MagicWandChunkNotFound(wand), /*InsufficientPermission(...)*/
               v1)(Q)
+          case (s1, _, _, None, v1) => Q(s1, h, True, v1)
         }
 
       case ast.AccessPredicate(loc @ ast.FieldAccess(eRcvr, field), ePerm)
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index cb2e6674f..1eb0b7169 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -9,7 +9,7 @@ package viper.silicon.rules
 import viper.silicon.Config.JoinMode
 import viper.silver.ast
 import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationError, VerifierWarning}
-import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, PreconditionInAppFalse}
+import viper.silver.verifier.errors.{ErrorWrapperWithExampleTransformer, Internal, PreconditionInAppFalse}
 import viper.silver.verifier.reasons._
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces._
@@ -57,7 +57,7 @@ trait EvaluationRules extends SymbolicExecutionRules {
                      name: String,
                      pve: PartialVerificationError,
                      v: Verifier)
-                    (Q: (State, Seq[Var], Seq[Term], Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Verifier) => VerificationResult)
+                    (Q: (State, Seq[Var], Seq[Term], Option[(Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]))], Verifier) => VerificationResult)
                     : VerificationResult
 }
 
@@ -722,7 +722,7 @@ object evaluator extends EvaluationRules {
         }
         val name = s"prog.$posString"
         evalQuantified(s, qantOp, eQuant.variables, Nil, Seq(body), Some(eTriggers), name, pve, v){
-          case (s1, tVars, _, Seq(tBody), tTriggers, (tAuxGlobal, tAux), v1) =>
+          case (s1, tVars, _, Some((Seq(tBody), tTriggers, (tAuxGlobal, tAux))), v1) =>
             val tAuxHeapIndep = tAux.flatMap(v.quantifierSupporter.makeTriggersHeapIndependent(_, v1.decider.fresh))
 
             v1.decider.prover.comment("Nested auxiliary terms: globals (aux)")
@@ -742,6 +742,13 @@ object evaluator extends EvaluationRules {
 
             val tQuant = Quantification(qantOp, tVars, tBody, tTriggers, name, quantWeight)
             Q(s1, tQuant, v1)
+          case (s1, _, _, None, v1) =>
+            // This should not happen unless the current path is dead.
+            if (v1.decider.checkSmoke(true)) {
+              Unreachable()
+            } else {
+              createFailure(pve.dueTo(InternalReason(sourceQuant, "Quantifier evaluation failed.")), v1, s1)
+            }
         }
 
       case fapp @ ast.FuncApp(funcName, eArgs) =>
@@ -1114,7 +1121,15 @@ object evaluator extends EvaluationRules {
                      name: String,
                      pve: PartialVerificationError,
                      v: Verifier)
-                    (Q: (State, Seq[Var], Seq[Term], Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Verifier) => VerificationResult)
+                    (Q: (State,
+                         Seq[Var], /* Variables from vars */
+                         Seq[Term], /* Terms from es1 */
+                         Option[ /* None if es2 or trigger evaluation did not result in a term because es1 is unsatisfiable */
+                           (Seq[Term], /* Terms from es2 */
+                            Seq[Trigger], /* Triggers from optTriggers */
+                            (Seq[Term], Seq[Quantification])) /* Global and non-global auxiliary assumptions */
+                         ],
+                         Verifier) => VerificationResult)
                     : VerificationResult = {
 
     val localVars = vars map (_.localVar)
@@ -1125,23 +1140,37 @@ object evaluator extends EvaluationRules {
                     quantifiedVariables = tVars ++ s.quantifiedVariables,
                     recordPossibleTriggers = true,
                     possibleTriggers = Map.empty) // TODO: Why reset possibleTriggers if they are merged with s.possibleTriggers later anyway?
-    type R = (State, Seq[Term], Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Map[ast.Exp, Term])
+    type R = (State, Seq[Term], Option[(Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Map[ast.Exp, Term])])
     executionFlowController.locallyWithResult[R](s1, v)((s2, v1, QB) => {
        val preMark = v1.decider.setPathConditionMark()
       evals(s2, es1, _ => pve, v1)((s3, ts1, v2) => {
         val bc = And(ts1)
+        // ME: If bc is unsatisfiable, we are assuming false here. In that case, evaluating es2 and the triggers
+        // may not return any value (e.g. if es2 contains a field read for which we don't have permission, a smoke
+        // check succeeds, then the continuation for evals(es2) is never invoked). This caused issue #842.
+        // In this case, we return None.
         v2.decider.setCurrentBranchCondition(bc, Some(viper.silicon.utils.ast.BigAnd(es1)))
-        evals(s3, es2, _ => pve, v2)((s4, ts2, v3) => {
+        var es2AndTriggerTerms: Option[(Seq[Term], Seq[Trigger], (Seq[Term], Seq[Quantification]), Map[ast.Exp, Term])] = None
+        var finalState = s3
+        val es2AndTriggerResult = evals(s3, es2, _ => pve, v2)((s4, ts2, v3) => {
           evalTriggers(s4, optTriggers.getOrElse(Nil), pve, v3)((s5, tTriggers, _) => { // TODO: v4 isn't forward - problem?
             val (auxGlobals, auxNonGlobalQuants) =
               v3.decider.pcs.after(preMark).quantified(quant, tVars, tTriggers, s"$name-aux", isGlobal = false, bc)
             val additionalPossibleTriggers: Map[ast.Exp, Term] =
               if (s.recordPossibleTriggers) s5.possibleTriggers else Map()
-            QB((s5, ts1, ts2, tTriggers, (auxGlobals, auxNonGlobalQuants), additionalPossibleTriggers))})})})
-    }){case (s2, ts1, ts2, tTriggers, (tAuxGlobal, tAux), additionalPossibleTriggers) =>
-      val s3 = s.copy(possibleTriggers = s.possibleTriggers ++ additionalPossibleTriggers)
+            es2AndTriggerTerms = Some((ts2, tTriggers, (auxGlobals, auxNonGlobalQuants), additionalPossibleTriggers)) // QB((s5, ts1, Some((ts2, tTriggers, (auxGlobals, auxNonGlobalQuants), additionalPossibleTriggers))))
+            finalState = s5
+            Success()
+          })})
+        es2AndTriggerResult combine QB((finalState, ts1, es2AndTriggerTerms))
+      })
+    }){
+      case (s2, ts1, Some((ts2, tTriggers, (tAuxGlobal, tAux), additionalPossibleTriggers))) =>
+        val s3 = s.copy(possibleTriggers = s.possibleTriggers ++ additionalPossibleTriggers)
                 .preserveAfterLocalEvaluation(s2)
-      Q(s3, tVars, ts1, ts2, tTriggers, (tAuxGlobal, tAux), v)
+        Q(s3, tVars, ts1, Some((ts2, tTriggers, (tAuxGlobal, tAux))), v)
+      case (s2, ts1, None) =>
+        Q(s2, tVars, ts1, None, v)
     }
   }
 
diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala
index 51096a3b4..e23472e23 100644
--- a/src/main/scala/rules/HavocSupporter.scala
+++ b/src/main/scala/rules/HavocSupporter.scala
@@ -104,7 +104,7 @@ object havocSupporter extends SymbolicExecutionRules {
       pve   = pve,
       v     = v)
     {
-      case (s1, tVars, Seq(tCond), tArgs, Seq(), _, v1) =>
+      case (s1, tVars, Seq(tCond), Some((tArgs, Seq(), _)), v1) =>
         // Seq() represents an empty list of Triggers
         // TODO: unnamed argument is (tAuxGlobal, tAux). How should these be handled?
 
@@ -154,6 +154,7 @@ object havocSupporter extends SymbolicExecutionRules {
 
             Q(s1.copy(h = Heap(newChunks)), v1)
         }
+      case (s1, _, _, None, v1) => Q(s1, v1)
     }
   }
 
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 7794de9c0..33d8a1126 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -411,7 +411,7 @@ object producer extends ProductionRules {
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
         evalQuantified(s, Forall, forall.variables, Seq(cond), Seq(acc.loc.rcv, acc.perm), optTrigger, qid, pve, v) {
-          case (s1, qvars, Seq(tCond), Seq(tRcvr, tPerm), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
+          case (s1, qvars, Seq(tCond), Some((Seq(tRcvr, tPerm), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
             val tSnap = sf(sorts.FieldValueFunction(v1.symbolConverter.toSort(acc.loc.field.typ), acc.loc.field.name), v1)
 //            v.decider.assume(PermAtMost(tPerm, FullPerm()))
             quantifiedChunkSupporter.produce(
@@ -432,6 +432,7 @@ object producer extends ProductionRules {
               QPAssertionNotInjective(acc.loc),
               v1
             )(Q)
+          case (s1, _, _, None, v1) => Q(s1, v1)
         }
 
       case QuantifiedPermissionAssertion(forall, cond, acc: ast.PredicateAccessPredicate) =>
@@ -442,7 +443,7 @@ object producer extends ProductionRules {
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
         evalQuantified(s, Forall, forall.variables, Seq(cond), acc.perm +: acc.loc.args, optTrigger, qid, pve, v) {
-          case (s1, qvars, Seq(tCond), Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals), v1) =>
+          case (s1, qvars, Seq(tCond), Some((Seq(tPerm, tArgs @ _*), tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
             val tSnap = sf(sorts.PredicateSnapFunction(s1.predicateSnapMap(predicate), predicate.name), v1)
             quantifiedChunkSupporter.produce(
               s1,
@@ -464,6 +465,7 @@ object producer extends ProductionRules {
               QPAssertionNotInjective(acc.loc),
               v1
             )(Q)
+          case (s1, _, _, None, v1) => Q(s1, v1)
         }
 
       case QuantifiedPermissionAssertion(forall, cond, wand: ast.MagicWand) =>
@@ -474,7 +476,7 @@ object producer extends ProductionRules {
           else Some(forall.triggers)
         val qid = MagicWandIdentifier(wand, s.program).toString
         evalQuantified(s, Forall, forall.variables, Seq(cond), bodyVars, optTrigger, qid, pve, v) {
-          case (s1, qvars, Seq(tCond), tArgs, tTriggers, (auxGlobals, auxNonGlobals), v1) =>
+          case (s1, qvars, Seq(tCond), Some((tArgs, tTriggers, (auxGlobals, auxNonGlobals))), v1) =>
             val tSnap = sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v1)
             quantifiedChunkSupporter.produce(
               s1,
@@ -496,6 +498,7 @@ object producer extends ProductionRules {
               QPAssertionNotInjective(wand),
               v1
             )(Q)
+          case (s1, _, _, None, v1) => Q(s1, v1)
         }
 
       case _: ast.InhaleExhaleExp =>