diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9a06cff266e221b0459b7d23e9417b4940ec5743..d936a4e3ac73612e62fa15e4eb3ba15102d1c6fb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -309,12 +309,19 @@ trait AbstractZ3Solver extends Solver {
         newAST
       }
       case v @ Variable(id) => z3Vars.get(id) match {
-        case Some(ast) => ast
+        case Some(ast) => 
+          ast
         case None => {
-          val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
-          z3Vars = z3Vars + (id -> newAST)
-          variables += (v -> newAST)
-          newAST
+          variables.getB(v) match {
+            case Some(ast) =>
+              ast
+
+            case None =>
+              val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
+              z3Vars = z3Vars + (id -> newAST)
+              variables += (v -> newAST)
+              newAST
+          }
         }
       }
 
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index d76cff69b1a630718632f70e8684ff2426506cd2..366037b2a68d37f2f2a0e03439b30fe3074be75d 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -76,6 +76,18 @@ object ConversionPhase extends UnitPhase[Program] {
    *    choose(x => post(x))
    *  }
    *
+   * 4) Functions that have only a choose as body gets their spec from the choose. 
+   *
+   *  def foo(a: T) = {
+   *    choose(x => post(a, x))
+   *  }
+   *
+   *  gets converted to:
+   *
+   *  def foo(a: T) = {
+   *    choose(x => post(a, x))
+   *  } ensuring { x => post(a, x) }
+   *
    */
 
   def convert(e : Expr, ctx : LeonContext) : Expr = {
@@ -115,7 +127,7 @@ object ConversionPhase extends UnitPhase[Program] {
       }
     }
 
-    body match {
+    val fullBody = body match {
       case Some(body) =>
         var holes  = List[Identifier]()
 
@@ -172,6 +184,14 @@ object ConversionPhase extends UnitPhase[Program] {
         val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
         withPrecondition(Choose(newPost), pre)
     }
+
+    // extract spec from chooses at the top-level
+    fullBody match {
+      case Choose(spec) =>
+        withPostcondition(fullBody, Some(spec))
+      case _ =>
+        fullBody
+    }
   }
 
 
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 77b451094ae1451ce7e46c9e3312488c7c398058..1dfddd0ca025caf3c7faafce3904c304be362f43 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -4,7 +4,6 @@ package synthesis
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.Constructors._
-import evaluators._
 import purescala.Common._
 import repair._
 import leon.utils.ASCIIHelpers._
@@ -175,9 +174,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
   }
 
   def filterIns(expr: Expr): ExamplesBank = {
-    val ev = new DefaultEvaluator(hctx.sctx.context, hctx.sctx.program)
-
-    filterIns(m => ev.eval(expr, m).result == Some(BooleanLiteral(true)))
+    filterIns(m => hctx.sctx.defaultEvaluator.eval(expr, m).result == Some(BooleanLiteral(true)))
   }
 
   def filterIns(pred: Map[Identifier, Expr] => Boolean): ExamplesBank = {
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index bb90d2a268411c44e9dfdbde013886b7db5b56d9..b01077ce751f6b53e397b15eb3d5126e560d1b56 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -6,6 +6,7 @@ package synthesis
 import solvers._
 import solvers.combinators._
 import purescala.Definitions.{Program, FunDef}
+import evaluators._
 
 /**
  * This is global information per entire search, contains necessary information
@@ -22,6 +23,10 @@ case class SynthesisContext(
   val rules = settings.rules
 
   val solverFactory = SolverFactory.getFromSettings(context, program)
+
+  lazy val defaultEvaluator = {
+    new DefaultEvaluator(context, program)
+  }
 }
 
 object SynthesisContext {
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 294c6e1374fa09ed6e54690aecfb4661b5073d04..7ed08608763f7a461c6c6eb66de6561fbd9fc85e 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -11,32 +11,43 @@ import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Definitions._
-import solvers._
 
 case object ADTSplit extends Rule("ADT Split.") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(200L))
+    // We approximate knowledge of types based on facts found at the top-level
+    // we don't care if the variables are known to be equal or not, we just
+    // don't want to split on two variables for which only one split
+    // alternative is viable. This should be much less expensive than making
+    //  calls to a solver for each pair.
+    var facts = Map[Identifier, CaseClassType]()
+
+    def addFacts(e: Expr): Unit = e match {
+      case Equals(Variable(a), CaseClass(cct, _))         => facts += a -> cct
+      case IsInstanceOf(Variable(a), cct: CaseClassType)  => facts += a -> cct
+      case _ =>
+    }
+
+    val TopLevelAnds(as) = and(p.pc, p.phi)
+    for (e <- as) {
+      addFacts(e)
+    }
 
     val candidates = p.as.collect {
       case IsTyped(id, act @ AbstractClassType(cd, tpes)) =>
 
-        val optCases = for (dcd <- cd.knownDescendants.sortBy(_.id.name)) yield dcd match {
+        val optCases = cd.knownDescendants.sortBy(_.id.name).collect {
           case ccd : CaseClassDef =>
             val cct = CaseClassType(ccd, tpes)
-            val toSat = and(p.pc, IsInstanceOf(Variable(id), cct))
 
-            val isImplied = solver.solveSAT(toSat) match {
-              case (Some(false), _) => true
-              case _ => false
-            }
-
-            if (!isImplied) {
-              Some(ccd)
+            if (facts contains id) {
+              if (cct == facts(id)) {
+                Seq(ccd)
+              } else {
+                Nil
+              }
             } else {
-              None
+              Seq(ccd)
             }
-          case _ =>
-            None
         }
 
         val cases = optCases.flatten
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f3fa5947d0c8cb8092f9d8fc032ca71c12cc2846..eb91692442f0e5bd0c94ec8e5e04d9255b06f920 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -43,14 +43,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
     val sctx = hctx.sctx
     val ctx  = sctx.context
 
-
     // CEGIS Flags to activate or deactivate features
     val useOptTimeout    = sctx.settings.cegisUseOptTimeout.getOrElse(true)
     val useVanuatoo      = sctx.settings.cegisUseVanuatoo.getOrElse(false)
-    val useShrink        = sctx.settings.cegisUseShrink.getOrElse(true)
+    val useShrink        = sctx.settings.cegisUseShrink.getOrElse(false)
 
     // Limits the number of programs CEGIS will specifically validate individually
-    val validateUpTo     = 5
+    val validateUpTo     = 3
 
     // Shrink the program when the ratio of passing cases is less than the threshold
     val shrinkThreshold  = 1.0/2
@@ -314,6 +313,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
       private val cTreeFd = new FunDef(FreshIdentifier("cTree", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), p.outType)
 
+      private val solFd = new FunDef(FreshIdentifier("solFd", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), p.outType)
+
       private val phiFd = new FunDef(FreshIdentifier("phiFd", alwaysShowUniqueID = true), Seq(), p.as.map(id => ValDef(id)), BooleanType)
 
 
@@ -321,13 +322,20 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
         val outerSolution = {
           new PartialSolution(hctx.search.g, true)
-            .solutionAround(hctx.currentNode)(FunctionInvocation(cTreeFd.typed, p.as.map(_.toVariable)))
+            .solutionAround(hctx.currentNode)(FunctionInvocation(solFd.typed, p.as.map(_.toVariable)))
             .getOrElse(ctx.reporter.fatalError("Unable to get outer solution"))
         }
 
-        val program0 = addFunDefs(sctx.program, Seq(cTreeFd, phiFd) ++ outerSolution.defs, hctx.ci.fd)
+        val program0 = addFunDefs(sctx.program, Seq(cTreeFd, solFd, phiFd) ++ outerSolution.defs, hctx.ci.fd)
 
         cTreeFd.body = None
+
+        solFd.fullBody = Ensuring(
+          FunctionInvocation(cTreeFd.typed, p.as.map(_.toVariable)),
+          Lambda(p.xs.map(ValDef(_)), p.phi)
+        )
+
+
         phiFd.body   = Some(
           letTuple(p.xs,
                    FunctionInvocation(cTreeFd.typed, p.as.map(_.toVariable)),
@@ -349,7 +357,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
           // We freshen/duplicate every functions, except these two as they are
           // fresh anyway and we refer to them directly.
-          case `cTreeFd` | `phiFd` =>
+          case `cTreeFd` | `phiFd` | `solFd` =>
             None
 
           case fd =>
@@ -454,13 +462,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
           //println("Solving for: "+cnstr.asString)
 
-          val solverf = SolverFactory.default(ctx, innerProgram).withTimeout(cexSolverTo)
+          val solverf = SolverFactory.getFromSettings(ctx, innerProgram).withTimeout(cexSolverTo)
           val solver  = solverf.getNewSolver()
           try {
             solver.assertCnstr(cnstr)
             solver.check match {
               case Some(true) =>
-                excludeProgram(bs)
+                excludeProgram(bs, true)
                 val model = solver.getModel
                 //println("Found counter example: ")
                 //for ((s, v) <- model) {
@@ -499,8 +507,24 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
       var excludedPrograms = ArrayBuffer[Set[Identifier]]()
 
       // Explicitly remove program computed by bValues from the search space
-      def excludeProgram(bValues: Set[Identifier]): Unit = {
-        val bvs = bValues.filter(isBActive)
+      //
+      // If the bValues comes from models, we make sure the bValues we exclude
+      // are minimal we make sure we exclude only Bs that are used.
+      def excludeProgram(bValues: Set[Identifier], isMinimal: Boolean): Unit = {
+        val bs = bValues.filter(isBActive)
+
+        def filterBTree(c: Identifier): Set[Identifier] = {
+          (for ((b, _, subcs) <- cTree(c) if bValues(b)) yield {
+           Set(b) ++ subcs.flatMap(filterBTree)
+          }).toSet.flatten
+        }
+
+        val bvs = if (isMinimal) {
+          bs
+        } else {
+          rootCs.flatMap(filterBTree).toSet
+        }
+
         excludedPrograms += bvs
       }
 
@@ -513,19 +537,21 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
        * First phase of CEGIS: solve for potential programs (that work on at least one input)
        */
       def solveForTentativeProgram(): Option[Option[Set[Identifier]]] = {
-        val solverf = SolverFactory.default(ctx, programCTree).withTimeout(exSolverTo)
+        val solverf = SolverFactory.getFromSettings(ctx, programCTree).withTimeout(exSolverTo)
         val solver  = solverf.getNewSolver()
         val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
-        //debugCExpr(cTree)
 
-        //println(" --- PhiFD ---")
-        //println(phiFd.fullBody.asString(ctx))
+        //println("Program: ")
+        //println("-"*80)
+        //println(programCTree.asString)
 
         val toFind = and(innerPc, cnstr)
         //println(" --- Constraints ---")
-        //println(" - "+toFind)
+        //println(" - "+toFind.asString)
         try {
-          solver.assertCnstr(andJoin(bsOrdered.map(b => if (bs(b)) b.toVariable else Not(b.toVariable))))
+          //TODO: WHAT THE F IS THIS?
+          //val bsOrNotBs = andJoin(bsOrdered.map(b => if (bs(b)) b.toVariable else Not(b.toVariable)))
+          //solver.assertCnstr(bsOrNotBs)
           solver.assertCnstr(toFind)
 
           for ((c, alts) <- cTree) {
@@ -536,26 +562,25 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
             }
 
             if (activeBs.nonEmpty) {
-              //println(" - "+andJoin(either))
+              //println(" - "+andJoin(either).asString)
               solver.assertCnstr(andJoin(either))
 
               val oneOf = orJoin(activeBs.map(_.toVariable))
-              //println(" - "+oneOf)
+              //println(" - "+oneOf.asString)
               solver.assertCnstr(oneOf)
             }
           }
 
-          //println(" -- Excluded:")
           //println(" -- Active:")
           val isActive = andJoin(bsOrdered.filterNot(isBActive).map(id => Not(id.toVariable)))
-          //println("  - "+isActive)
+          //println("  - "+isActive.asString)
           solver.assertCnstr(isActive)
 
           //println(" -- Excluded:")
           for (ex <- excludedPrograms) {
             val notThisProgram = Not(andJoin(ex.map(_.toVariable).toSeq))
 
-            //println(f"  - $notThisProgram%-40s ("+getExpr(ex)+")")
+            //println(f"  - ${notThisProgram.asString}%-40s ("+getExpr(ex)+")")
             solver.assertCnstr(notThisProgram)
           }
 
@@ -565,7 +590,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
               val bModel = bs.filter(b => model.get(b).contains(BooleanLiteral(true)))
 
+              //println("Tentative model: "+model.asString)
+              //println("Tentative model: "+bModel.filter(isBActive).map(_.asString).toSeq.sorted)
               //println("Tentative expr: "+getExpr(bModel))
+
               Some(Some(bModel))
 
             case Some(false) =>
@@ -591,7 +619,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
        * Second phase of CEGIS: verify a given program by looking for CEX inputs
        */
       def solveForCounterExample(bs: Set[Identifier]): Option[Option[Seq[Expr]]] = {
-        val solverf = SolverFactory.default(ctx, programCTree).withTimeout(cexSolverTo)
+        val solverf = SolverFactory.getFromSettings(ctx, programCTree).withTimeout(cexSolverTo)
         val solver  = solverf.getNewSolver()
         val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
 
@@ -601,6 +629,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           solver.assertCnstr(innerPc)
           solver.assertCnstr(Not(cnstr))
 
+          //println("*"*80)
+          //println(Not(cnstr))
+          //println(innerPc)
+          //println("*"*80)
+          //println(programCTree.asString)
+          //println("*"*80)
+          //Console.in.read()
+
           solver.check match {
             case Some(true) =>
               val model = solver.getModel
@@ -685,17 +721,6 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
          */
         val nTests = if (p.pc == BooleanLiteral(true)) 50 else 20
 
-        /*
-        val inputGenerator: FreeableIterator[Example] = {
-          val sff = {
-            (ctx: LeonContext, pgm: Program) =>
-              SolverFactory.default(ctx, pgm).withTimeout(exSolverTo)
-          }
-          new SolverDataGen(sctx.context, sctx.program, sff).generateFor(p.as, p.pc, nTests, nTests).map {
-            InExample(_)
-          }
-        } */
-
         val inputGenerator: Iterator[Example] = if (useVanuatoo) {
           new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000).map(InExample)
         } else {
@@ -813,15 +838,15 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
               }
 
               if (doFilter && !(nPassing < nInitial * shrinkThreshold && useShrink)) {
+                sctx.reporter.debug("Excluding "+wrongPrograms.size+" programs")
                 wrongPrograms.foreach {
-                  ndProgram.excludeProgram
+                  ndProgram.excludeProgram(_, true)
                 }
               }
             }
 
             // CEGIS Loop at a given unfolding level
             while (result.isEmpty && !skipCESearch && !interruptManager.isInterrupted) {
-
               ndProgram.solveForTentativeProgram() match {
                 case Some(Some(bs)) =>
                   // Should we validate this program with Z3?
@@ -833,18 +858,21 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
                       // make sure by validating this candidate with z3
                       true
                     } else {
+                      println("testing failed ?!")
                       // One valid input failed with this candidate, we can skip
-                      ndProgram.excludeProgram(bs)
+                      ndProgram.excludeProgram(bs, false)
                       false
                     }
                   } else {
                     // No inputs or capability to test, we need to ask Z3
                     true
                   }
+                  sctx.reporter.debug("Found tentative model (Validate="+validateWithZ3+")!")
 
                   if (validateWithZ3) {
                     ndProgram.solveForCounterExample(bs) match {
                       case Some(Some(inputsCE)) =>
+                        sctx.reporter.debug("Found counter-example:"+inputsCE)
                         val ce = InExample(inputsCE)
                         // Found counter example!
                         baseExampleInputs += ce
@@ -853,7 +881,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
                         if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(ce))) {
                           skipCESearch = true
                         } else {
-                          ndProgram.excludeProgram(bs)
+                          ndProgram.excludeProgram(bs, false)
                         }
 
                       case Some(None) =>
@@ -863,6 +891,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
                       case None =>
                         // We are not sure
+                        sctx.reporter.debug("Unknown")
                         if (useOptTimeout) {
                           // Interpret timeout in CE search as "the candidate is valid"
                           sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index bc62dbba88c8b7dea8b6aaefc5879dfc3909774f..132ea9f766720d776af801e36ac58cc1f6b87b73 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -6,6 +6,7 @@ package rules
 
 import leon.purescala.Common.Identifier
 import purescala.Expressions._
+import purescala.Extractors._
 import purescala.Constructors._
 
 import solvers._
@@ -14,31 +15,31 @@ import scala.concurrent.duration._
 
 case object EqualitySplit extends Rule("Eq. Split") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
+    // We approximate knowledge of equality based on facts found at the top-level
+    // we don't care if the variables are known to be equal or not, we just
+    // don't want to split on two variables for which only one split
+    // alternative is viable. This should be much less expensive than making
+    //  calls to a solver for each pair.
+    var facts = Set[Set[Identifier]]()
 
-    val candidates = p.as.groupBy(_.getType).mapValues(_.combinations(2).filter {
-      case List(a1, a2) =>
-        val toValEQ = implies(p.pc, Equals(Variable(a1), Variable(a2)))
-
-        val impliesEQ = solver.solveSAT(Not(toValEQ)) match {
-          case (Some(false), _) => true
-          case _ => false
-        }
-
-        if (!impliesEQ) {
-          val toValNE = implies(p.pc, not(Equals(Variable(a1), Variable(a2))))
+    def addFacts(e: Expr): Unit = e match {
+      case Not(e) => addFacts(e)
+      case LessThan(Variable(a), Variable(b))      => facts += Set(a,b)
+      case LessEquals(Variable(a), Variable(b))    => facts += Set(a,b)
+      case GreaterThan(Variable(a), Variable(b))   => facts += Set(a,b)
+      case GreaterEquals(Variable(a), Variable(b)) => facts += Set(a,b)
+      case Equals(Variable(a), Variable(b))        => facts += Set(a,b)
+      case _ =>
+    }
 
-          val impliesNE = solver.solveSAT(Not(toValNE)) match {
-            case (Some(false), _) => true
-            case _ => false
-          }
+    val TopLevelAnds(as) = and(p.pc, p.phi)
+    for (e <- as) {
+      addFacts(e)
+    }
 
-          !impliesNE
-        } else {
-          false
-        }
-      case _ => false
-    }).values.flatten
+    val candidates = p.as.groupBy(_.getType).mapValues{ as =>
+      as.combinations(2).filterNot(facts contains _.toSet)
+    }.values.flatten
 
     candidates.flatMap {
       case List(a1, a2) =>
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 292e99de80d4cf7eb3351621edde3587645b0402..ed8a285ff3f0a52a61760598ac742013d0e77f5d 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -7,57 +7,42 @@ package rules
 import purescala.Expressions._
 import purescala.Types._
 import purescala.Constructors._
-
-import solvers._
+import purescala.Extractors._
+import purescala.Common._
 
 import scala.concurrent.duration._
 
 case object InequalitySplit extends Rule("Ineq. Split.") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
-    val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(50.millis))
+    // We approximate knowledge of equality based on facts found at the top-level
+    // we don't care if the variables are known to be equal or not, we just
+    // don't want to split on two variables for which only one split
+    // alternative is viable. This should be much less expensive than making
+    //  calls to a solver for each pair.
+    var facts = Set[Set[Identifier]]()
+
+    def addFacts(e: Expr): Unit = e match {
+      case Not(e) => addFacts(e)
+      case LessThan(Variable(a), Variable(b))      => facts += Set(a,b)
+      case LessEquals(Variable(a), Variable(b))    => facts += Set(a,b)
+      case GreaterThan(Variable(a), Variable(b))   => facts += Set(a,b)
+      case GreaterEquals(Variable(a), Variable(b)) => facts += Set(a,b)
+      case Equals(Variable(a), Variable(b))        => facts += Set(a,b)
+      case _ =>
+    }
+
+    val TopLevelAnds(as) = and(p.pc, p.phi)
+    for (e <- as) {
+      addFacts(e)
+    }
 
     val argsPairs = p.as.filter(_.getType == IntegerType).combinations(2) ++
                     p.as.filter(_.getType == Int32Type).combinations(2)
 
-    val candidates = argsPairs.toList.filter {
-      case List(a1, a2) =>
-        val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2)))
-
-        val impliesLT = solver.solveSAT(not(toValLT)) match {
-          case (Some(false), _) => true
-          case _ => false
-        }
-
-        if (!impliesLT) {
-          val toValGT = implies(p.pc, GreaterThan(Variable(a1), Variable(a2)))
-
-          val impliesGT = solver.solveSAT(not(toValGT)) match {
-            case (Some(false), _) => true
-            case _ => false
-          }
-
-          if (!impliesGT) {
-            val toValEQ = implies(p.pc, Equals(Variable(a1), Variable(a2)))
-
-            val impliesEQ = solver.solveSAT(not(toValEQ)) match {
-              case (Some(false), _) => true
-              case _ => false
-            }
-
-            !impliesEQ
-          } else {
-            false
-          }
-        } else {
-          false
-        }
-      case _ => false
-    }
-
+    val candidates = argsPairs.toList.filter { case List(a1, a2) => !(facts contains Set(a1, a2)) }
 
     candidates.flatMap {
       case List(a1, a2) =>
-
         val subLT = p.copy(pc = and(LessThan(Variable(a1), Variable(a2)), p.pc),
                            eb = p.qeb.filterIns(LessThan(Variable(a1), Variable(a2))))
         val subEQ = p.copy(pc = and(Equals(Variable(a1), Variable(a2)), p.pc),
diff --git a/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala b/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..64cb3b70b062ba30ccf6223af587ed85c9b4ff88
--- /dev/null
+++ b/src/test/scala/leon/integration/solvers/GlobalVariablesSuite.scala
@@ -0,0 +1,74 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.integration.solvers
+
+import leon.test._
+import leon.test.helpers._
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.purescala.ExprOps._
+import leon.purescala.Constructors._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.LeonContext
+
+import leon.solvers._
+import leon.solvers.smtlib._
+import leon.solvers.combinators._
+import leon.solvers.z3._
+
+class GlobalVariablesSuite extends LeonTestSuiteWithProgram with ExpressionsDSL {
+
+  val sources = List(
+    """|import leon.lang._
+       |import leon.annotation._
+       |
+       |object GlobalVariables {
+       |
+       |  def test(i: BigInt): BigInt = {
+       |    0 // will be replaced
+       |  }
+       |} """.stripMargin
+  )
+
+  val getFactories: Seq[(String, (LeonContext, Program) => Solver)] = {
+    (if (SolverFactory.hasNativeZ3) Seq(
+      ("fairz3",   (ctx: LeonContext, pgm: Program) => new FairZ3Solver(ctx, pgm))
+    ) else Nil) ++
+    (if (SolverFactory.hasZ3)       Seq(
+      ("smt-z3",   (ctx: LeonContext, pgm: Program) => new UnrollingSolver(ctx, pgm, new SMTLIBZ3Solver(ctx, pgm)))
+    ) else Nil) ++
+    (if (SolverFactory.hasCVC4)     Seq(
+      ("smt-cvc4", (ctx: LeonContext, pgm: Program) => new UnrollingSolver(ctx, pgm, new SMTLIBCVC4Solver(ctx, pgm)))
+    ) else Nil)
+  }
+
+  // Check that we correctly extract several types from solver models
+  for ((sname, sf) <- getFactories) {
+    test(s"Global Variables in $sname") { implicit fix =>
+      val ctx = fix._1
+      val pgm = fix._2
+
+      pgm.lookup("GlobalVariables.test") match {
+        case Some(fd: FunDef) =>
+          val b0 = FreshIdentifier("B", BooleanType);
+          fd.body = Some(IfExpr(b0.toVariable, bi(1), bi(-1)))
+
+          val cnstr = LessThan(FunctionInvocation(fd.typed, Seq(bi(42))), bi(0))
+          val solver = sf(ctx, pgm)
+          solver.assertCnstr(And(b0.toVariable, cnstr))
+
+          try { 
+            if (solver.check != Some(false)) {
+              fail("Global variables not correctly handled.")
+            }
+          } finally {
+            solver.free()
+          }
+        case _ =>
+          fail("Function with global body not found")
+      }
+
+    }
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Delete.scala b/testcases/synthesis/etienne-thesis/List/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..46f0710878d25a30e679f034ff07f985078950d1
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Delete.scala
@@ -0,0 +1,41 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Delete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  //def delete(in1: List, v: BigInt): List = {
+  //  in1 match {
+  //    case Cons(h,t) =>
+  //      if (h == v) {
+  //        delete(t, v)
+  //      } else {
+  //        Cons(h, delete(t, v))
+  //      }
+  //    case Nil =>
+  //      Nil
+  //  }
+  //} ensuring { content(_) == content(in1) -- Set(v) }
+
+  def delete(in1: List, v: BigInt) = choose {
+    (out : List) =>
+      content(out) == content(in1) -- Set(v)
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Diff.scala b/testcases/synthesis/etienne-thesis/List/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9fb3ade9558a7db175c6056efb9bf724f487d7ca
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Diff.scala
@@ -0,0 +1,50 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Diff {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def delete(in1: List, v: BigInt): List = {
+    in1 match {
+      case Cons(h,t) =>
+        if (h == v) {
+          delete(t, v)
+        } else {
+          Cons(h, delete(t, v))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { content(_) == content(in1) -- Set(v) }
+
+  // def diff(in1: List, in2: List): List = {
+  //   in2 match {
+  //     case Nil =>
+  //       in1
+  //     case Cons(h, t) =>
+  //       diff(delete(in1, h), t)
+  //   }
+  // } ensuring { content(_) == content(in1) -- content(in2) }
+
+  def diff(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) -- content(in2)
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Insert.scala b/testcases/synthesis/etienne-thesis/List/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..48c38f4df0098410814f3ed27038c9c36c0d6532
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Insert.scala
@@ -0,0 +1,28 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Insert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  //def insert(in1: List, v: BigInt): List = {
+  //  Cons(v, in1)
+  //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def insert(in1: List, v: BigInt) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ Set(v)
+  }
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Split.scala b/testcases/synthesis/etienne-thesis/List/Split.scala
new file mode 100644
index 0000000000000000000000000000000000000000..47793c0810c5b4b7884bf2689511e39232eba268
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Split.scala
@@ -0,0 +1,39 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def splitSpec(list : List, res : (List,List)) : Boolean = {
+    val s1 = size(res._1)
+    val s2 = size(res._2)
+    abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+    content(res._1) ++ content(res._2) == content(list) 
+  }
+
+  def abs(i : BigInt) : BigInt = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => splitSpec(list, res) }
+  }
+
+  // case (h1, (h2, t)) => (h1 :: split(t)._1, h2 :: split(t)._2)
+
+}
diff --git a/testcases/synthesis/etienne-thesis/List/Union.scala b/testcases/synthesis/etienne-thesis/List/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d6a5fa579f5745f00e469f19ee853da15d4fece7
--- /dev/null
+++ b/testcases/synthesis/etienne-thesis/List/Union.scala
@@ -0,0 +1,37 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Union {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1)+ size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  // def union(in1: List, in2: List): List = {
+  //   in1 match {
+  //     case Cons(h, t) =>
+  //       Cons(h, union(t, in2))
+  //     case Nil =>
+  //       in2
+  //   }
+  // } ensuring { content(_) == content(in1) ++ content(in2) }
+
+  def union(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ content(in2)
+  }
+}