diff --git a/silver b/silver
index 07d7c4fbd..e47320f60 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 07d7c4fbdfc5a0aa9db6f3dd38d75e8ea34c1243
+Subproject commit e47320f60caef480d255ad0a0da0a4ed922919ba
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 255cec1c6..c5e85cc60 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -227,7 +227,7 @@ object evaluator extends EvaluationRules {
                     Q(s2, fvfLookup, v1)}
               }
             case _ =>
-              val (_, smDef1, pmDef1) =
+              val (s2, smDef1, pmDef1) =
                 quantifiedChunkSupporter.heapSummarisingMaps(
                   s = s1,
                   resource = fa.field,
@@ -236,12 +236,12 @@ object evaluator extends EvaluationRules {
                   optSmDomainDefinitionCondition =  None,
                   optQVarsInstantiations = None,
                   v = v1)
-              if (s1.heapDependentTriggers.contains(fa.field)){
+              if (s2.heapDependentTriggers.contains(fa.field)){
                 val trigger = FieldTrigger(fa.field.name, smDef1.sm, tRcvr)
                 v1.decider.assume(trigger)
               }
               val permCheck =
-                if (s1.triggerExp) {
+                if (s2.triggerExp) {
                   True
                 } else {
                   val totalPermissions = PermLookup(fa.field.name, pmDef1.pm, tRcvr)
@@ -249,14 +249,13 @@ object evaluator extends EvaluationRules {
                 }
               v1.decider.assert(permCheck) {
                 case false =>
-                  createFailure(pve dueTo InsufficientPermission(fa), v1, s1)
+                  createFailure(pve dueTo InsufficientPermission(fa), v1, s2)
                 case true =>
                   val smLookup = Lookup(fa.field.name, smDef1.sm, tRcvr)
                   val fr2 =
-                    s1.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, smLookup)
+                    s2.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, smLookup)
                                        .recordFvfAndDomain(smDef1)
-                  val s3 = s1.copy(functionRecorder = fr2/*,
-                                   smCache = smCache1*/)
+                  val s3 = s2.copy(functionRecorder = fr2)
                   Q(s3, smLookup, v1)}
               }})
 
diff --git a/src/test/scala/SiliconTestsSmokeDetection.scala b/src/test/scala/SiliconTestsSmokeDetection.scala
new file mode 100644
index 000000000..e58752a3c
--- /dev/null
+++ b/src/test/scala/SiliconTestsSmokeDetection.scala
@@ -0,0 +1,13 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2022 ETH Zurich.
+
+package viper.silicon.tests
+
+class SiliconTestsSmokeDetection extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("smoke")
+
+  override val commandLineArguments: Seq[String] = Seq("--enableSmokeDetection")
+}