diff --git a/silver b/silver
index 5611fcbd1..5f5c02202 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 5611fcbd13209be062344a26c0cbdbb3a728c92a
+Subproject commit 5f5c02202030b67c0cf90d8540d26ca3d71c9bd6
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 0570c926c..1b3e82e63 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -1029,6 +1029,12 @@ object evaluator extends EvaluationRules {
           Option.when(withExp)(s.relevantQuantifiedVariables.map(_._2.get)), v))((s4, r4, v4)
           => Q(s4, r4._1, r4._2, v4))
 
+      case ast.Asserting(eAss, eIn) =>
+        consume(s, eAss, pve, v)((s2, _, v2) => {
+          val s3 = s2.copy(g = s.g, h = s.h)
+          eval(s3, eIn, pve, v2)(Q)
+        })
+
       /* Sequences */
 
       case ast.SeqContains(e0, e1) => evalBinOp(s, e1, e0, SeqIn, pve, v)((s1, t, e1New, e0New, v1) =>
diff --git a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
index 02dd6d9f0..4b70d2140 100644
--- a/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
+++ b/src/main/scala/supporters/functions/HeapAccessReplacingExpressionTranslator.scala
@@ -128,6 +128,7 @@ class HeapAccessReplacingExpressionTranslator(symbolConverter: SymbolConverter,
       case loc: ast.LocationAccess => getOrFail(data.locToSnap, loc, toSort(loc.typ), Option.when(Verifier.config.enableDebugging())(extractPTypeFromExp(loc)))
       case ast.Unfolding(_, eIn) => translate(toSort)(eIn)
       case ast.Applying(_, eIn) => translate(toSort)(eIn)
+      case ast.Asserting(_, eIn) => translate(toSort)(eIn)
 
       case eFApp: ast.FuncApp =>
         val silverFunc = program.findFunction(eFApp.funcname)