diff --git a/testcases/synthesis/repair/PropLogic/PropLogic5.scala b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b411082fdb6c777c8b4fdfbb83e4f7cc67a5e11
--- /dev/null
+++ b/testcases/synthesis/repair/PropLogic/PropLogic5.scala
@@ -0,0 +1,52 @@
+// Fails
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+
+object SemanticsPreservation { 
+
+  sealed abstract class Formula
+  case class And(lhs : Formula, rhs : Formula) extends Formula
+  case class Or(lhs : Formula, rhs : Formula) extends Formula
+  case class Not(f: Formula) extends Formula
+  case class Const(v: Boolean) extends Formula
+  case class Literal(id: Int) extends Formula
+
+  def size(f : Formula) : Int = { f match {
+    case And(l,r) => 1 + size(l) + size(r)
+    case Or(l,r) =>  1 + size(l) + size(r)
+    case Not(e) => 1 + size(e)
+    case _ => 1
+  }} ensuring { _ >= 0 }
+
+  def eval(formula: Formula)(implicit trueVars : Set[Int]): Boolean = formula match {
+    case And(lhs, rhs) => eval(lhs) && eval(rhs)
+    case Or(lhs, rhs)  => eval(lhs) || eval(rhs)
+    case Not(f) => !eval(f)
+    case Const(v) => v
+    case Literal(id) => trueVars contains id
+  }
+
+  def nnf(formula : Formula) : Formula = { formula match {
+    case Not(And(lhs,rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+    case Not(Or(lhs,rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+    case Not(Const(v)) => Const(!v)
+    case Not(Not(e)) => nnf(e)
+    case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+    case Or(lhs, rhs)  => formula//And(nnf(lhs), nnf(rhs)) // FIXME should be Or
+    case other => other 
+  }} ensuring { res => 
+    isNNF(res) && ((formula, res) passes {
+      case Or(Not(Const(c)), Not(Literal(l))) => Or(Const(!c), Not(Literal(l)))
+    })
+  }
+
+  def isNNF(f : Formula) : Boolean = f match {
+    case Not(Literal(_)) => true
+    case Not(_) => false
+    case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+    case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+    case _ => true
+  }
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree10.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..93d5b61e9288be38928b9a01dfd3092889bfeef3
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree10.scala
@@ -0,0 +1,143 @@
+import leon._ 
+import lang._
+import annotation._
+
+object RedBlackTree { 
+  sealed abstract class Color
+  case object Red extends Color
+  case object Black extends Color
+ 
+  sealed abstract class Tree
+  case object Empty extends Tree
+  case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+  def content(t: Tree) : Set[Int] = t match {
+    case Empty => Set.empty
+    case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree) : Int = t match {
+    case Empty => 0
+    case Node(_, l, v, r) => size(l) + 1 + size(r)
+  }
+
+  /* We consider leaves to be black by definition */
+  def isBlack(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(Black,_,_,_) => true
+    case _ => false
+  }
+
+  def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+  }
+
+  def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+  }
+
+  def blackBalanced(t : Tree) : Boolean = t match {
+    case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+    case Empty => true
+  }
+
+  def blackHeight(t : Tree) : Int = t match {
+    case Empty => 1
+    case Node(Black, l, _, _) => blackHeight(l) + 1
+    case Node(Red, l, _, _) => blackHeight(l)
+  }
+ 
+    
+  // <<insert element x into the tree t>>
+  def ins(x: Int, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+    t match {
+      case Empty => Node(Red,Empty,x,Empty)
+      case Node(c,a,y,b) =>
+        if      (x < y)  balance(c, ins(x, a), y, b)
+        else if (x == y) Node(c,a,y,b)
+        else             balance(c,a,y,ins(x, b))
+    }
+  } ensuring (res => 
+    content(res) == content(t) ++ Set(x) && 
+    size(t) <= size(res) && 
+    size(res) <= size(t) + 1 && 
+    redDescHaveBlackChildren(res) && 
+    blackBalanced(res) 
+  )
+
+  def makeBlack(n: Tree): Tree = {
+    require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+    n match {
+      case Node(Red,l,v,r) => Node(Black,l,v,r)
+      case _ => n
+    }
+  } 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 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(
+    //   Node(c,a,x,b) match {
+    //     case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) => 
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) => 
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case t => redDescHaveBlackChildren(t)
+    //   }
+    // )
+    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(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(Black,c,xV,d))  // FIXME: xV instead of zV in right node
+      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,xV,d))  // FIXME: xV instead of zV in right node
+      case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) => 
+        Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+      case Node(c,a,xV,b) => Node(c,a,xV,b)
+    }
+  } ensuring (res => content(res) == content(Node(c,a,x,b))) //&& redDescHaveBlackChildren(res))
+
+  // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+  //   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(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(Black,c,zV,d))
+  //     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))) => 
+  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+  //   }
+  // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
index 1bad0be2912c369f3237b24f832758e6d70aba86..8ceec4415eefa3fe4e9e2f694b30e90b0c3457e4 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree3.scala
@@ -88,7 +88,7 @@ object RedBlackTree {
 //    ins(x, t)
 //  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
-  def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+  /*def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
     // require(
     //   Node(c,a,x,b) match {
     //     case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
@@ -126,6 +126,7 @@ object RedBlackTree {
       case Node(c,a,xV,b) => Node(c,a,xV,b)
     }
   } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
+  */
 
   // FIXME : says buggy, so I uncommented it!
   def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
index bea0f7bbc04fcc365cc49971155273bdead45351..531a5b491e6f529bc7390842af5822af6f75b153 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree5.scala
@@ -75,7 +75,7 @@ object RedBlackTree {
       case Node(Red,l,v,r) => Node(Black,l,v,r)
       case _ => n
     }
-  } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+  } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) && content(res) == content(n) )
 
   def add(x: Int, t: Tree): Tree = {
     require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
index ff1284daebc5e589b845d17f0b2b2cc51869c2d3..66b83042888f4e72bbde73cd4940edceeb935df7 100644
--- a/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree7.scala
@@ -75,7 +75,7 @@ object RedBlackTree {
       case Node(Red,l,v,r) => Node(Black,l,v,r) 
       case Node(Black,l,v,r) => Node(Red,l,v,r) // FIXME : Red instead of Black
     }
-  } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+  } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) && content(res) == content(n) )
 
   def add(x: Int, t: Tree): Tree = {
     require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree8.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cff237c6f16bbd9f8f1a9000d333966b2ef4a555
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree8.scala
@@ -0,0 +1,143 @@
+import leon._ 
+import lang._
+import annotation._
+
+object RedBlackTree { 
+  sealed abstract class Color
+  case object Red extends Color
+  case object Black extends Color
+ 
+  sealed abstract class Tree
+  case object Empty extends Tree
+  case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+  def content(t: Tree) : Set[Int] = t match {
+    case Empty => Set.empty
+    case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree) : Int = t match {
+    case Empty => 0
+    case Node(_, l, v, r) => size(l) + 1 + size(r)
+  }
+
+  /* We consider leaves to be black by definition */
+  def isBlack(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(Black,_,_,_) => true
+    case _ => false
+  }
+
+  def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+  }
+
+  def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+  }
+
+  def blackBalanced(t : Tree) : Boolean = t match {
+    case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+    case Empty => true
+  }
+
+  def blackHeight(t : Tree) : Int = t match {
+    case Empty => 1
+    case Node(Black, l, _, _) => blackHeight(l) + 1
+    case Node(Red, l, _, _) => blackHeight(l)
+  }
+ 
+    
+  // <<insert element x into the tree t>>
+  def ins(x: Int, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+    t match {
+      case Empty => Node(Red,Empty,x,Empty)
+      case Node(c,a,y,b) =>
+        if      (x < y)  balance(c, ins(x, a), y, b)
+        else if (x == y) Node(c,a,y,b)
+        else             balance(c,a,y,ins(x, b))
+    }
+  } ensuring (res => 
+    content(res) == content(t) ++ Set(x) && 
+    size(t) <= size(res) && 
+    size(res) <= size(t) + 1 && 
+    redDescHaveBlackChildren(res) && 
+    blackBalanced(res) 
+  )
+
+  def makeBlack(n: Tree): Tree = {
+    require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+    n match {
+      case Node(Red,l,v,r) => Node(Black,l,v,r)
+      case _ => n
+    }
+  } 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 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(
+    //   Node(c,a,x,b) match {
+    //     case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) => 
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) => 
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case t => redDescHaveBlackChildren(t)
+    //   }
+    // )
+    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(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),xV,Node(Black,c,zV,d))  // FIXME: xV instead of yV in top node
+      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))) => 
+        Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+      case Node(c,a,xV,b) => Node(c,a,xV,b)
+    }
+  } ensuring (res => content(res) == content(Node(c,a,x,b))) //&& redDescHaveBlackChildren(res))
+
+  // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+  //   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(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(Black,c,zV,d))
+  //     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))) => 
+  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+  //   }
+  // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/synthesis/repair/RedBlackTree/RedBlackTree9.scala b/testcases/synthesis/repair/RedBlackTree/RedBlackTree9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4d8e1f39d07d8c667a0fa733d6d09fce2569f1a4
--- /dev/null
+++ b/testcases/synthesis/repair/RedBlackTree/RedBlackTree9.scala
@@ -0,0 +1,143 @@
+import leon._ 
+import lang._
+import annotation._
+
+object RedBlackTree { 
+  sealed abstract class Color
+  case object Red extends Color
+  case object Black extends Color
+ 
+  sealed abstract class Tree
+  case object Empty extends Tree
+  case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+  def content(t: Tree) : Set[Int] = t match {
+    case Empty => Set.empty
+    case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree) : Int = t match {
+    case Empty => 0
+    case Node(_, l, v, r) => size(l) + 1 + size(r)
+  }
+
+  /* We consider leaves to be black by definition */
+  def isBlack(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(Black,_,_,_) => true
+    case _ => false
+  }
+
+  def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(Black, l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case Node(Red, l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+  }
+
+  def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty => true
+    case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+  }
+
+  def blackBalanced(t : Tree) : Boolean = t match {
+    case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+    case Empty => true
+  }
+
+  def blackHeight(t : Tree) : Int = t match {
+    case Empty => 1
+    case Node(Black, l, _, _) => blackHeight(l) + 1
+    case Node(Red, l, _, _) => blackHeight(l)
+  }
+ 
+    
+  // <<insert element x into the tree t>>
+  def ins(x: Int, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+    t match {
+      case Empty => Node(Red,Empty,x,Empty)
+      case Node(c,a,y,b) =>
+        if      (x < y)  balance(c, ins(x, a), y, b)
+        else if (x == y) Node(c,a,y,b)
+        else             balance(c,a,y,ins(x, b))
+    }
+  } ensuring (res => 
+    content(res) == content(t) ++ Set(x) && 
+    size(t) <= size(res) && 
+    size(res) <= size(t) + 1 && 
+    redDescHaveBlackChildren(res) && 
+    blackBalanced(res) 
+  )
+
+  def makeBlack(n: Tree): Tree = {
+    require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+    n match {
+      case Node(Red,l,v,r) => Node(Black,l,v,r)
+      case _ => n
+    }
+  } 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 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(
+    //   Node(c,a,x,b) match {
+    //     case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) => 
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) => 
+    //       redNodesHaveBlackChildren(a) &&
+    //       redNodesHaveBlackChildren(b) &&
+    //       redNodesHaveBlackChildren(c) &&
+    //       redNodesHaveBlackChildren(d)
+    //     case t => redDescHaveBlackChildren(t)
+    //   }
+    // )
+    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(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(Black,c,xV,d))  // FIXME: xV instead of zV in right node
+      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))) => 
+        Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+      case Node(c,a,xV,b) => Node(c,a,xV,b)
+    }
+  } ensuring (res => content(res) == content(Node(c,a,x,b))) //&& redDescHaveBlackChildren(res))
+
+  // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+  //   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(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(Black,c,zV,d))
+  //     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))) => 
+  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
+  //   }
+  // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}