diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 61693206b0fcf55fdae8beec1814b56792563c5b..fd3af5c50278afd441804b0962a36613f4c89d41 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -171,7 +171,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
           rec(pathVar, body)
 
         case e @ Ensuring(_, _) =>
-          rec(pathVar, e.toAssert) 
+          rec(pathVar, e.toAssert)
 
         case l @ Let(i, e : Lambda, b) =>
           val re = rec(pathVar, e) // guaranteed variable!
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 3959e2265f67ac446faf4e2d4ea81fd8f617b562..321f1234a5db3e671c207838993f8a6a06ea6126 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -361,6 +361,9 @@ trait AbstractZ3Solver
       }
 
       case Waypoint(_, e, _) => rec(e)
+      case a @ Assert(cond, err, body) =>
+        rec(IfExpr(cond, body, Error(a.getType, err.getOrElse("Assertion failed")).setPos(a.getPos)).setPos(a.getPos))
+
       case e @ Error(tpe, _) => {
         val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
         // Might introduce dupplicates (e), but no worries here