diff --git a/silver b/silver
index 65ec3412..65819343 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 65ec3412bb9118a8c465462c94dab6d0d53da5f4
+Subproject commit 658193435975a0deb3598eb8f03a8f3f4d43ee0b
diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala
index 11272560..57b4facb 100644
--- a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala
+++ b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala
@@ -253,9 +253,11 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt
       case sil.Seqn(ss, scopedDecls) =>
         val locals = scopedDecls.collect {case l: sil.LocalVarDecl => l}
         locals map (v => mainModule.env.define(v.localVar)) // add local variables to environment
-        val s =
+        val s = {
+          MaybeCommentBlock("Havoc scoped variables", locals map (lv => Havoc(mainModule.env.get(lv.localVar)))) ++
           MaybeCommentBlock("Assumptions about local variables", locals map (a => mainModule.allAssumptionsAboutValue(a.typ, mainModule.translateLocalVarDecl(a), true))) ++
           Seqn(ss map (st => translateStmt(st, statesStack, allStateAssms, duringPackage)))
+        }
         locals map (v => mainModule.env.undefine(v.localVar)) // remove local variables from environment
         // return to avoid adding a comment, and to avoid the extra 'assumeGoodState'
         return s