diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 72f3b09e886f51c8c1868d87606f451167115605..6523a1104127c174edf5c1e9d994be27b797d421 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -136,7 +136,8 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
 
             val (solSize, proof) = solutions.headOption match {
               case Some((sol, trusted)) =>
-                val totalSolSize = formulaSize(sol.toSimplifiedExpr(ctx, program))
+                val solExpr = sol.toSimplifiedExpr(ctx, program)
+                val totalSolSize = formulaSize(solExpr)
                 (locSize+totalSolSize-fSize, if (trusted) "$\\chmark$" else "")
               case _ =>
                 (0, "X")
@@ -147,7 +148,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
             val fw = new java.io.FileWriter("repair-report.txt", true)
 
             try {
-              fw.write(f"$date:  $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%.2f &  & ${timeSynth/1000.0}%.2f & $proof%7s \\\\\n")
+              fw.write(f"$date:  $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%2.1f &  ${timeSynth/1000.0}%2.1f & $proof%7s \\\\\n")
             } finally {
               fw.close
             }
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 911a06ce5d0cfa0f98c8613a8880e483e3b49b9a..bafed6ec2bab51539bfc0547563bbad2aeea873e 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -99,7 +99,7 @@ class Synthesizer(val context : LeonContext,
       val fw = new java.io.FileWriter("synthesis-report.txt", true)
 
       try {
-        fw.write(f"$date:  $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%.2f \\\\\n")
+        fw.write(f"$date:  $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%2.1f \\\\\n")
       } finally {
         fw.close
       }
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
index f49670ddc31632343fea32f1b8d39ca288f214d4..6323496df930172e84b71bf5c55006eb33767c6a 100644
--- a/testcases/repair/Compiler/Compiler4.scala
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -150,7 +150,7 @@ object Desugar {
     case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
     case Trees.And  (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0)) 
     case Trees.Or   (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
-    case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIMXE should be 0
+    case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIXME should be 0
     case Trees.Eq(lhs, rhs) =>
       Eq(desugar(lhs), desugar(rhs))
     case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index b6cb5e276741be29d86da86b7c43cbe7e1639c62..1ee180b3331e9cc51df34207b8ab5b6fec9b710b 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -78,16 +78,18 @@ sealed abstract class List[T] {
       }
   }
 
-  def drop(i: BigInt): List[T] = { (this, i) match {
-    case (Nil(), _) => Nil[T]()
-    case (Cons(h, t), i) =>
-      // FIXME
-      //if (i == 0) {
-      //  Cons(h, t)
-      //} else {
-        t.drop(i-1)
-      //}
-  }} ensuring { ((this, i), _) passes { 
+  def drop(i: BigInt): List[T] = {
+    (this, i) match {
+      case (Nil(), _) => Nil[T]()
+      case (Cons(h, t), i) =>
+        // FIXME
+        if (i != 0) {
+          Cons(h, t)
+        } else {
+          t.drop(i-1)
+        }
+    }
+  } ensuring { ((this, i), _) passes { 
     case (Cons(_, Nil()), BigInt(42)) => Nil()
     case (l@Cons(_, _), BigInt(0)) => l
     case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 3c109722c774ca76dfbff35b8124003566d5c94b..f13f91da3d55d7cdcf0eb0d3ef41027e1a8e94d8 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -97,7 +97,7 @@ sealed abstract class List[T] {
     case Nil() => Nil[T]()
     case Cons(h, t) =>
       val r = t.replace(from, to)
-      if (h != from) {
+      if (h != from) { // FIXME
         Cons(to, r)
       } else {
         Cons(h, r)
diff --git a/testcases/repair/runTests.sh b/testcases/repair/runTests.sh
index 5ad1c857cde7fbe7c92b38c1edd017d68a4dede5..fb92991cba1b5b0725b794f6d8cfd6c14f95cd05 100755
--- a/testcases/repair/runTests.sh
+++ b/testcases/repair/runTests.sh
@@ -16,22 +16,24 @@ echo "#           Category,                 File,             function, p.S, fuS
 
 #All benchmarks:
 
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler1.scala   | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler2.scala   | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler3.scala   | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler4.scala   | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler5.scala   | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala   | tee -a $fullLog
-#
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap3.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap4.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap5.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap6.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap7.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert   testcases/repair/Heap/Heap8.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN    testcases/repair/Heap/Heap9.scala        | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap10.scala       | tee -a $fullLog
-#
+echo "=====================================================================" >> repair-report.txt
+
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler1.scala   | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler2.scala   | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler3.scala   | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler4.scala   | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar  testcases/repair/Compiler/Compiler5.scala   | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala   | tee -a $fullLog
+
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap3.scala        | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap4.scala        | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap5.scala        | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap6.scala        | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap7.scala        | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge    testcases/repair/Heap/Heap10.scala       | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert   testcases/repair/Heap/Heap8.scala        | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN    testcases/repair/Heap/Heap9.scala        | tee -a $fullLog
+
 #./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
 #./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
 #./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf      testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog