diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala
index 11272560..21975a6b 100644
--- a/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala
+++ b/src/main/scala/viper/carbon/modules/impls/DefaultStmtModule.scala
@@ -207,8 +207,9 @@ class DefaultStmtModule(val verifier: Verifier) extends StmtModule with SimpleSt
         //handled by LoopModule
         Nil
       case i@sil.If(cond, thn, els) =>
+        val condTr = if(allStateAssms == TrueLit()) { translateExpInWand(cond) } else { allStateAssms ==> translateExpInWand(cond) }
         checkDefinedness(cond, errors.IfFailed(cond), insidePackageStmt = insidePackageStmt) ++
-        If((allStateAssms) ==> translateExpInWand(cond),
+        If(condTr,
           translateStmt(thn, statesStack, allStateAssms, insidePackageStmt),
           translateStmt(els, statesStack, allStateAssms, insidePackageStmt))
       case sil.Label(name, _) => {