diff --git a/src/orderedsets/TreeOperations.scala b/src/orderedsets/TreeOperations.scala
index eae52fe58a7bbb953598f682a59eae57e31d588d..af94736e68285092752fb40ea01e45c3877ebd00 100644
--- a/src/orderedsets/TreeOperations.scala
+++ b/src/orderedsets/TreeOperations.scala
@@ -38,7 +38,7 @@ object TreeOperations {
         if (ex == newExpr)
           if (recursive) rec(ex, ex) else ex
         else
-        if (recursive) rec(newExpr) else newExpr
+          if (recursive) rec(newExpr) else newExpr
       }
       case None => ex match {
         case l@Let(i, e, b) => {
@@ -98,7 +98,8 @@ object TreeOperations {
         case f@FiniteSet(elems) => {
           FiniteSet(elems.map(rec(_))).setType(f.getType)
         }
-        case _ => ex
+        case Terminal() => ex   // Ok
+        case _ => error("Unsupported case in searchAndReplace : " + ex.getClass) // Missed case
       }
     }
 
@@ -126,4 +127,74 @@ object TreeOperations {
       None
     }
   }
+  
+  // 'Lazy' rewriter
+  // 
+  // Hoists if expressions to the top level and
+  // transforms them to disjunctions.
+  //
+  // The implementation is totally brain-teasing
+  def rewrite(expr: Expr): Expr =
+    rewrite(expr, ex => ex)
+  
+  private def rewrite(expr: Expr, context: Expr => Expr): Expr = expr match {
+    case IfExpr(_c, _t, _e) =>
+      rewrite(_c, c =>
+        rewrite(_t, t =>
+          rewrite(_e, e =>
+            Or(And(c, context(t)), And(negate(c), context(e)))
+          )))
+    case And(_exs) =>
+      rewrite_*(_exs, exs =>
+        context(And(exs)))
+    case Or(_exs) =>
+      rewrite_*(_exs, exs =>
+        context(Or(exs)))
+    case Not(_ex) =>
+      rewrite(_ex, ex => 
+        context(Not(ex)))
+    case f@FunctionInvocation(fd, _args) =>
+      rewrite_*(_args, args =>
+        context(FunctionInvocation(fd, args) setType f.getType))
+    case u@UnaryOperator(_t, recons) =>
+      rewrite(_t, t =>
+        context(recons(t) setType u.getType))
+    case b@BinaryOperator(_t1, _t2, recons) =>
+      rewrite(_t1, t1 => 
+        rewrite(_t2, t2 => 
+          context(recons(t1, t2) setType b.getType)))
+    case c@CaseClass(cd, _args) =>
+      rewrite_*(_args, args =>
+        context(CaseClass(cd, args) setType c.getType))
+    case c@CaseClassSelector(_cc, sel) =>
+      rewrite(_cc, cc =>
+        context(CaseClassSelector(cc, sel) setType c.getType))
+    case f@FiniteSet(_elems) =>
+      rewrite_*(_elems, elems =>
+        context(FiniteSet(elems) setType f.getType))
+    case Terminal() =>
+      context(expr)
+    case _ => // Missed case
+      error("Unsupported case in rewrite : " + expr.getClass)
+  }
+  
+  private def rewrite_*(exprs: Seq[Expr], context: Seq[Expr] => Expr): Expr =
+    exprs match {
+      case Nil => context(Nil)
+      case _t :: _ts =>
+        rewrite(_t, t => rewrite_*(_ts, ts => context(t +: ts)))
+    }
+  
+  // This should rather be a marker interface, but I don't want
+  // to change Trees.scala without Philippe's permission.
+  object Terminal {
+    def unapply(expr: Expr): Boolean = expr match {
+      case Variable(_) | ResultVariable() | OptionNone(_) | EmptySet(_) | EmptyMultiset(_) | EmptyMap(_, _) | NilList(_) => true
+      case _: Literal[_] => true
+      case _ => false
+    }
+  }
+  
+  
+  
 }
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index 91bc6bd6bbe91c4726f2edeff45938a35a70d5f9..f51e4a7fcfc3b9aba4b442a8aefcee7ed30bb06f 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/src/orderedsets/UnifierMain.scala
@@ -33,11 +33,13 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
   // None means you don't know.
   //
   def solve(exprWithLets: Expr): Option[Boolean] = {
-    val expr = expandLets(exprWithLets)
+    val exprWithIfs = expandLets(exprWithLets)
+    val negatedExprWithIfs = negate(exprWithIfs)
+    val expr = rewrite(negatedExprWithIfs)
     //println(rpp(expr))
     try {
       var counter = 0
-      for (conjunction <- dnf(negate(expr))) {
+      for (conjunction <- dnf(expr)) {
         counter += 1
         //reporter.info("Solving conjunction " + counter)
         //println(rpp(And(conjunction)))
@@ -93,7 +95,19 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
 
   def checkIsSupported(expr: Expr) {
     def check(ex: Expr): Option[Expr] = ex match {
-      case IfExpr(_, _, _) | Let(_, _, _) | MatchExpr(_, _) =>
+      case Let(_, _, _) | MatchExpr(_, _) =>
+        throw ConversionException(ex, "Unifier does not support this expression")
+      case IfExpr(_, _, _) =>
+       
+       println
+       println("--- BEFORE ---")
+       println(rpp(expr))
+       println
+       println("--- AFTER ---")
+       println(rpp(rewrite(expr)))
+       println
+         
+      
         throw ConversionException(ex, "Unifier does not support this expression")
       case _ => None
     }
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index e72ae013d0bf5039a59b9e38aaf624f6109227e6..a8116240bfb4d5af4d5d8dee9bee6ed2e3040457 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -86,7 +86,7 @@ object BinarySearchTree {
         n
       }
     }
-  } //ensuring (contents(_) == contents(tree) ++ Set(value))
+  } ensuring (contents(_) == contents(tree) ++ Set(value))
 
   def dumbInsert(tree: Tree): Node = {
     tree match {