diff --git a/src/orderedsets/Main.scala b/src/orderedsets/Main.scala
index 4a01636218aba3e0a13eda6d00e2f7d8101c574b..8eafc12ac23855d65112615134632921ad0c65d1 100644
--- a/src/orderedsets/Main.scala
+++ b/src/orderedsets/Main.scala
@@ -105,6 +105,7 @@ object ExprToASTConverter {
   }
 
   private def toSetTerm(expr: Expr): AST.Term = expr match {
+    case ResultVariable() if isSetType(expr.getType) => Symbol("#res", Symbol.SetType)
     case Variable(id) if isSetType(id.getType) => Symbol(id.name, Symbol.SetType)
     case EmptySet(_) => AST.emptyset
     case FiniteSet(elems) if elems forall {_.getType == Int32Type} => AST.Op(UNION, (elems map toIntTerm map {_.singleton}).toList)
@@ -112,10 +113,12 @@ object ExprToASTConverter {
     case SetIntersection(set1, set2) => toSetTerm(set1) ** toSetTerm(set2)
     case SetUnion(set1, set2) => toSetTerm(set1) ++ toSetTerm(set2)
     case SetDifference(set1, set2) => toSetTerm(set1) -- toSetTerm(set2)
-    case _ => throw ConversionException(expr, "Cannot convert to bapa< set term")
+    case Variable(_) => throw ConversionException(expr, "is a variable and cannot convert to bapa< set variable")
+    case _ => throw ConversionException(expr, "is of type " + expr.getType + ": Cannot convert to bapa< set term")
   }
 
   private def toIntTerm(expr: Expr): AST.Term = expr match {
+    case ResultVariable() if expr.getType == Int32Type => Symbol("#res", Symbol.IntType)
     case Variable(id) if id.getType == Int32Type => Symbol(id.name, Symbol.IntType)
     case IntLiteral(v) => AST.Lit(IntLit(v))
     case Plus(lhs, rhs) => toIntTerm(lhs) + toIntTerm(rhs)
diff --git a/src/orderedsets/UnifierMain.scala b/src/orderedsets/UnifierMain.scala
index 8f56d5c3d2f48f557ee996b4c649f2719d5d632c..2d92e4e896b6486b81a134a08c6b110458d7bc5d 100644
--- a/src/orderedsets/UnifierMain.scala
+++ b/src/orderedsets/UnifierMain.scala
@@ -5,6 +5,12 @@ import purescala.Reporter
 import purescala.Extensions.Solver
 import Reconstruction.Model
 
+import purescala._
+import Trees._
+import Common._
+import TypeTrees._
+import Definitions._
+
 case class IncompleteException(msg: String) extends Exception(msg)
 
 class UnifierMain(reporter: Reporter) extends Solver(reporter) {
@@ -14,6 +20,9 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
   val description = "Unifier for ADTs with abstractions"
   override val shortDescription = "Unifier"
 
+  var program:Program = null
+  override def setProgram(p: Program) = program = p
+
   // checks for V-A-L-I-D-I-T-Y !
   // Some(true) means formula is valid (negation is unsat)
   // Some(false) means formula is not valid (negation is sat)
@@ -29,7 +38,11 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
         //conjunction foreach println
         conjunction foreach checkIsSupported
         try {
-          solve(conjunction)
+          // restFormula is also a Sequence of conjunctions
+          val (varMap, restFormula) = solve(conjunction)
+          // TODO: Might contain multiple c_i ~= {} for a fixed i
+          val noAlphas = restFormula flatMap expandAlphas(varMap)
+          reporter.info("The resulting formula is " + noAlphas)
         } catch {        
           case UnificationImpossible(msg) =>
             reporter.info("Conjunction " + counter + " is UNSAT, unification impossible : " + msg)
@@ -57,6 +70,38 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
       
     }
   }
+
+  def isAlpha(varMap: Variable => Expr)(t: Expr): Option[Expr] = t match {
+    case FunctionInvocation(fd, Seq(v@ Variable(_))) => asCatamorphism(program, fd) match {
+      case None => None
+      case Some(lstMatch) => varMap(v) match {
+        case CaseClass(cd, args) => {
+          val (_, _, ids, rhs) = lstMatch.find( _._1 == cd).get
+          val repMap = Map( ids.map(id => Variable(id):Expr).zip(args): _* )
+          Some(searchAndReplace(repMap.get)(rhs))
+        }
+        case u @ Variable(_) => {
+          val c = Variable(FreshIdentifier("Coll", true)).setType(t.getType)
+          // TODO: Keep track of these variables for M1(t, c)
+          Some(c)
+        }
+        case _ => error("Bad substitution")
+      }
+      case _ => None
+    }
+    case _ => None
+  }
+
+
+  def expandAlphas(varMap: Variable => Expr)(e: Expr) : Seq[Expr] = isAlpha(varMap)(e) match {
+      case None => Seq(e) // Not a catamorphism
+      case Some(cata) =>  // cata is the Partially evaluated expression
+        // The original expression is not returned
+        var nonEmptySetsExpr = Seq.empty[Expr]
+        // SetEquals or just Equals?
+        searchAndReplace({case v@Variable(_) => nonEmptySetsExpr :+= Not(SetEquals(v, EmptySet(v.getType))); None; case _ => None})(cata)
+        nonEmptySetsExpr
+  }
   
   def checkIsSupported(expr: Expr) {
     def check(ex: Expr): Option[Expr] = ex match {
@@ -68,7 +113,10 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
   }
 
   
-  def solve(conjunction: Seq[Expr]) {
+  /* Returns a conjunction which contains the rest of the formula
+   * apart from the ADTs
+   */
+  def solve(conjunction: Seq[Expr]): (Variable => Expr, Seq[Expr]) = {
     val (treeEquations, rest) = separateADT(conjunction)
     
     /*
@@ -83,10 +131,9 @@ class UnifierMain(reporter: Reporter) extends Solver(reporter) {
     
     // The substitution function (returns identity if unmapped)
     def subst(v: Variable): Expr = substTable getOrElse (v, v)
-    
-    throw IncompleteException(null)
-    
-    ()
+
+    (subst, rest)
+
   }
   
   /* Step 1 : Do DNF transformation (done elsewhere) */
diff --git a/testcases/SetOperations.scala b/testcases/SetOperations.scala
index bf8c42fc0561a9b19da03a51390d27400e62340c..07d58548150bad372a866831198933899db54e84 100644
--- a/testcases/SetOperations.scala
+++ b/testcases/SetOperations.scala
@@ -39,6 +39,14 @@ object SetOperations {
             (a ** b ** c).size
   }
   
+  // OrderedBAPA verification with Min and Max
+  def expandSet(a: Set[Int]) : Set[Int] = {
+    require(a.size >= 1)
+    val x = a.min - 1
+    val y = a.max + 1
+    Set(x) ++ Set(y) ++ a
+  } ensuring {res => res.max > a.max && res.min < a.min}
+
   // .. but this can no longer be proved by the OrderedBAPA solver,
   // because "Set(b)" is neither a set of uninterpreted elements (pure BAPA)
   // nor it is a set of integers (ordered BAPA).