diff --git a/src/orderedsets/Main.scala b/src/orderedsets/Main.scala
index 5bb8e21a3d05211c4478eed807ce3de0a1eecfe1..f7f53a10ede162530c8166a9c7de665c3c055a49 100644
--- a/src/orderedsets/Main.scala
+++ b/src/orderedsets/Main.scala
@@ -104,10 +104,18 @@ object ExprToASTConverter {
 
   var formulaRelaxed = false
   
-  private def isSetType(_type: TypeTree) = _type match {
+  def isSetType(_type: TypeTree) = _type match {
     case SetType(_) => true
     case _ => false
   }
+  
+  def isAcceptableType(_type: TypeTree) = isSetType(_type) || _type == Int32Type
+
+  def makeEq(v: Variable, t: Expr) = v.getType match {
+    case Int32Type => Equals(v, t)
+    case tpe if isSetType(tpe) => SetEquals(v, t)
+    case _ => throw(new ConversionException(v, "is of type " + v.getType + " and cannot be handled by OrdBapa"))
+  }
 
   private def toSetTerm(expr: Expr): AST.Term = expr match {
     case ResultVariable() if isSetType(expr.getType) => Symbol("#res", Symbol.SetType)
diff --git a/src/orderedsets/TreeOperations.scala b/src/orderedsets/TreeOperations.scala
index d2380bbbfb48c792b6b60f2b2f411a33410a974b..68ffa10c8021b170449706d23712edb91bafa07e 100644
--- a/src/orderedsets/TreeOperations.scala
+++ b/src/orderedsets/TreeOperations.scala
@@ -95,6 +95,11 @@ object TreeOperations {
           else
             c
         }
+
+        case f @ FiniteSet(elems) => {
+          FiniteSet(elems.map(rec(_))).setType(f.getType)
+        }
+
         case _ => ex
       }
     }
@@ -123,4 +128,4 @@ object TreeOperations {
       None
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index 951279fbd7c982b9b682227bc641fe49f1d89f46..be3d3bf4d00de45b518a7652ee513bf657d052cb 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/src/orderedsets/UnifierMain.scala
@@ -39,12 +39,23 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
         conjunction foreach checkIsSupported
         try {
           // restFormula is also a Sequence of conjunctions
-          val (varMap, restFormula) = solve(conjunction)
+          val (substTable, treeEquations, restFormula) = solve(conjunction)
+          // The substitution function (returns identity if unmapped)
+          def varMap(v: Variable): Expr = substTable getOrElse (v, v)
+
           // TODO: Might contain multiple c_i ~= {} for a fixed i
           val noAlphas = restFormula flatMap expandAlphas(varMap)
           reporter.info("The resulting formula is " + noAlphas)
+
+          // Extracting only the needed equalities Fe (to avoid unnecessary relaxations)
+          // Assuming that all the inequalities which did not involve TermAlgebra are already
+          // in restFormula
+          val usefulEqns = substTable.filter(x => ExprToASTConverter.isAcceptableType(x._1.getType)).map(x => ExprToASTConverter.makeEq(x._1, x._2))
+
+          reporter.info("The useful equations are: " + substTable)
+          reporter.info("The tree equations are: " + treeEquations)
           // OrdBAPA finds the formula satisfiable
-          if((new Main(reporter)).solve(ExprToASTConverter(And(noAlphas.toList)))) {
+          if((new Main(reporter)).solve(ExprToASTConverter(And(noAlphas.toList ++ usefulEqns.toList ++ treeEquations.toList)))) {
             throw(new SatException(null))
           }  
         } catch {        
@@ -83,8 +94,9 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
           case CaseClass(cd, args) => {
             val (_, _, ids, rhs) = lstMatch.find( _._1 == cd).get
             val repMap = Map( ids.map(id => Variable(id):Expr).zip(args): _* )
-            reporter.warning("Converting " + t + " to " + rhs)
-            Some(searchAndReplace(repMap.get)(rhs))
+            val repRHS = searchAndReplace(repMap.get)(rhs)
+            reporter.warning("Converting " + t + " to " + repRHS + " with variables = " + getVars(repRHS))
+            Some(repRHS)
           }
           case u @ Variable(_) => {
             val c = Variable(FreshIdentifier("Coll", true)).setType(t.getType)
@@ -95,6 +107,7 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
         }
         case Seq(CaseClass(cd, _)) => 
           val (_, _, ids, rhs) = lstMatch.find( _._1 == cd).get
+          reporter.warning("Converting " + t + " to " + rhs)
           Some(rhs)
         case _ => error("Not a catamorphism.")
       }
@@ -102,6 +115,11 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
     case _ => None
   }
 
+  def getVars(t: Expr) = {
+    var varNames = Set.empty[String]
+    searchAndReplace({ case Variable(id) => varNames += id.uniqueName; None; case _ => None })(t)
+    varNames
+  }
 
   def expandAlphas(varMap: Variable => Expr)(e: Expr) : Seq[Expr] = {
     val partiallyEvaluated = searchAndReplace(isAlpha(varMap))(e)
@@ -111,9 +129,11 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
     }
     else { // partiallyEvaluated is the Partially evaluated expression
       reporter.warning(e + " found to contain one or more catamorphisms. Translated to: " + partiallyEvaluated)
+      reporter.warning(e + " had variables = " + getVars(e))
+      reporter.warning(partiallyEvaluated + " has variables = " + getVars(partiallyEvaluated))
       var nonEmptySetsExpr = Seq(partiallyEvaluated)
       // SetEquals or just Equals?
-      searchAndReplace({case v@Variable(_) => nonEmptySetsExpr :+= Not(SetEquals(v, EmptySet(v.getType))); None; case _ => None})(partiallyEvaluated)
+      searchAndReplace({case v@Variable(_) if ExprToASTConverter.isSetType(v.getType) => nonEmptySetsExpr :+= Not(SetEquals(v, EmptySet(v.getType))); None; case _ => None})(partiallyEvaluated)
       nonEmptySetsExpr
     }
   }
@@ -131,7 +151,7 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
   /* Returns a conjunction which contains the rest of the formula
    * apart from the ADTs
    */
-  def solve(conjunction: Seq[Expr]): (Variable => Expr, Seq[Expr]) = {
+  def solve(conjunction: Seq[Expr]): (Map[Variable, Expr], Seq[Expr], Seq[Expr]) = {
     val (treeEquations, rest) = separateADT(conjunction)
     
     /*
@@ -144,10 +164,8 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
     // The substitution table
     val substTable = ADTUnifier.unify(treeEquations)
     
-    // The substitution function (returns identity if unmapped)
-    def subst(v: Variable): Expr = substTable getOrElse (v, v)
 
-    (subst, rest)
+    (substTable, treeEquations, rest)
 
   }
   
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index 221441af7e0cda1ba186150712056b3499b3f83a..4121579298afb4e5c11b9506a1e1b3c574071031 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -90,6 +90,10 @@ object BinarySearchTree {
         case Node(l, e, r) => Node(dumbInsert(l), e, r)
       }} ensuring (contents(_) == contents(tree) ++ Set(0))
 
+    def createRoot(v: Int): Node = {
+        Node(Leaf(), v, Leaf())
+    } ensuring (contents(_) == Set(v))
+
 /*
     def remove(tree: Tree, value: Int) : Node = (tree match {
         case Leaf() => Node(Leaf(), value, Leaf())