diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index c29a2b19ee8475f9a2c03850022e5dcd02a5d06d..2c62fb5d48fbd315904a41e6f775413078bff185 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -82,9 +82,9 @@ class Analysis(val program: Program) {
       val vc = vcInfo.condition
 
       reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
-      // reporter.info("Verification condition (post) for ==== " + funDef.id + " ====")
+      reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
       // if(Settings.unrollingLevel == 0) {
-      //   reporter.info(simplifyLets(vc))
+      reporter.info(simplifyLets(vc))
       // } else {
       //   reporter.info("(not showing unrolled VCs)")
       // }
diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala
index b7e586a396495c10d7558fe872f1b7bd7ecbb1fe..5b16ad4ea494446e410d547a87f8803f913d0188 100644
--- a/src/purescala/DefaultTactic.scala
+++ b/src/purescala/DefaultTactic.scala
@@ -77,7 +77,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
             expr2
           }
         }
-        Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this))
+        Seq(new VerificationCondition(theExpr, functionDefinition, VCKind.Postcondition, this.asInstanceOf[DefaultTactic]))
       }
     }
   
@@ -110,7 +110,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
             withPrecIfDefined(path, newCall),
             function,
             VCKind.Precondition,
-            this).setPosInfo(fi)
+            this.asInstanceOf[DefaultTactic]).setPosInfo(fi)
         }).toSeq
       } else {
         Seq.empty
@@ -142,7 +142,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
             withPrecIfDefined(pc._1),
             function,
             VCKind.ExhaustiveMatch,
-            this).setPosInfo(pc._2.asInstanceOf[Error])
+            this.asInstanceOf[DefaultTactic]).setPosInfo(pc._2.asInstanceOf[Error])
         ).toSeq
       } else {
         Seq.empty
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 967899a1ec6f451cb88085a1931c2615cf41d99f..c9054fc0831b1c1d855111b42c8b85bc3e082903 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -726,6 +726,14 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
               assert(argsSize == 2)
               Times(rargs(0), rargs(1))
             }
+            case OpDiv => {
+              assert(argsSize == 2)
+              Division(rargs(0), rargs(1))
+            }
+            case OpIDiv => {
+              assert(argsSize == 2)
+              Division(rargs(0), rargs(1))
+            }
             case other => {
               System.err.println("Don't know what to do with this declKind : " + other)
               throw new CantTranslateException(t)