Fix Asserts in VCs in fairz3

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!

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