diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index c88913162d639bc84ae2b7d8599029898c3412cd..e5b257f077816aea9995a50c0c04195cd6b6c7b6 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -32,17 +32,23 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
 
   def repair() = {
     reporter.info(ASCIIHelpers.title("1. Discovering tests for "+fd.id))
+    val t1 = new Timer().start
     val (passingTests, failingTests) = discoverTests
 
     reporter.info(f" - Passing: ${passingTests.size}%3d")
     reporter.info(f" - Failing: ${failingTests.size}%3d")
 
+    reporter.info("Finished in "+t1.stop+"ms")
+
+
     reporter.info(ASCIIHelpers.title("2. Locating/Focusing synthesis problem"))
+    val t2 = new Timer().start
     val synth = getSynthesizer(passingTests, failingTests)
     val p     = synth.problem
 
     var solutions = List[Solution]()
 
+    reporter.info("Finished in "+t2.stop+"ms")
     reporter.info(ASCIIHelpers.title("3. Synthesizing"))
     reporter.info(p)
 
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic4.scala b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
index 20e44fe9258e2f6d59377fd8999f1ddc2b65dc1c..025c0a8b556c111b76362ea8133776f1f2cff82d 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic4.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
@@ -37,7 +37,7 @@ object SemanticsPreservation {
     case other => other 
   }} ensuring { res => 
     isNNF(res) && ((formula, res) passes {
-      case Or(Not(Const(c)), Not(Literal(l))) => Or(Const(c), Not(Literal(l)))
+      case Or(Not(Const(c)), Not(Literal(l))) => Or(Const(!c), Not(Literal(l)))
     })
   }
 
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
index 9480a168677d32336ffcaa2e2a6d912b01238917..e705ff4fabf095941f594200ef0e3f01ba2db833 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree1.scala
@@ -116,9 +116,9 @@ object RedBlackTree {
     // )
     Node(c,a,x,b) match {
       case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) => 
-        Node(Red,Node(Black,a,xV,b),yV,Node(Red,c,zV,d)) // FIXME: Last Red should be Black
+        Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
       case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) => 
-        Node(Red,Node(Black,a,xV,b),yV,Node(Red,c,zV,d)) // FIXME: as above
+        Node(Red,Node(Black,a,xV,b),yV,Node(Red,c,zV,d))  // FIXME: Last Red should be Black
       case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) => 
         Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
       case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) => 
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
index 6aa63cefd2323f2b5e297a2696627fe52152b678..d4675cadb43edffbc9eb395e373d5751a03e5ecc 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree2.scala
@@ -59,7 +59,7 @@ object RedBlackTree {
       case Node(c,a,y,b) =>
         if      (x < y)  Node(c, ins(x, a), y, b) // FIXME : forgot to balance
         else if (x == y) Node(c,a,y,b)
-        else             Node(c,a,y,ins(x, b)) // FIXME : as above
+        else             balance(c,a,y,ins(x, b))
     }
   } ensuring (res => 
     content(res) == content(t) ++ Set(x) && 
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
index 865c320ab250fa7ddd8bca514a737611b9393186..eb5dc7248a6690ff0114307f42d043a81b6509f2 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree6.scala
@@ -77,17 +77,15 @@ object RedBlackTree {
     }
   } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
 
+  //def add(x: Int, t: Tree): Tree = {
+  //  require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+  //  makeBlack(ins(x, t))
+  //} ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ 
   def add(x: Int, t: Tree): Tree = {
     require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
-    makeBlack(ins(x, t))
+    ins(x, t) // FIX: makeBlack(ins(x, t))
   } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
- 
-  // FIXME: uncommented this
-  def buggyAdd(x: Int, t: Tree): Tree = {
-    require(redNodesHaveBlackChildren(t))
-    // makeBlack(ins(x, t))
-    ins(x, t)
-  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
   def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
     // require(