diff --git a/build.sbt b/build.sbt
index 4fe1fed09e3957e2cf28679c6150909b77bb78f4..a7c534d6490c98e51b24f0921ce0e94a72607cd6 100644
--- a/build.sbt
+++ b/build.sbt
@@ -25,6 +25,7 @@ resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/release
 libraryDependencies ++= Seq(
     "org.scala-lang" % "scala-compiler" % "2.10.2",
     "org.scalatest" % "scalatest_2.10" % "2.0.M5b" % "test" excludeAll(ExclusionRule(organization="org.scala-lang")),
+    "junit" % "junit" % "4.8" % "test",
     "com.typesafe.akka" %% "akka-actor" % "2.2.0" excludeAll(ExclusionRule(organization="org.scala-lang"))
 )
 
diff --git a/src/main/scala/insynth/InSynth.scala b/src/main/scala/insynth/InSynth.scala
index ae6d24a7063b9c354b384035fd1286952519ed10..3646bad45635882b50c8fbb58d631688a5b60f6e 100644
--- a/src/main/scala/insynth/InSynth.scala
+++ b/src/main/scala/insynth/InSynth.scala
@@ -4,14 +4,13 @@ import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFact
 import insynth.reconstruction.codegen.CodeGenerator
 import insynth.reconstruction.Reconstructor
 
-import insynth.interfaces.Declaration
 import insynth.engine.InitialEnvironmentBuilder
 
+import insynth.leon.{ LeonDeclaration => Declaration }
 import insynth.leon.loader.LeonLoader
 import insynth.leon.LeonQueryBuilder
 
 import _root_.leon.purescala.Definitions.Program
-import _root_.leon.purescala.Trees.Hole
 import _root_.leon.purescala.TypeTrees.{ TypeTree => Type }
 
 import insynth.util.logging.HasLogger
@@ -21,13 +20,15 @@ import insynth.util.logging.HasLogger
  * @param program Leon program object that contains the hole
  * @param hole hole in the program on which the synthesis is called 
  */
-class InSynth(declarations: List[Declaration], goalType: Type, ordered: Boolean = true) extends HasLogger {
+class InSynth(_declarations: List[Declaration], goalType: Type, ordered: Boolean = true) extends HasLogger {
+  
+  def declarations = _declarations
   
 //  def this(program: Program, hole: Hole, ordered: Boolean) =
 //    this(new LeonLoader(program, hole).load, hole.getType, ordered)
     
-  def this(loader: LeonLoader, ordered: Boolean) =
-    this(loader.load, loader.hole.getType, ordered)
+  def this(loader: LeonLoader, goalType: Type, ordered: Boolean) =
+    this(loader.load, goalType, ordered)
   
   lazy val solver = new Solver(declarations, new LeonQueryBuilder(goalType))
   
@@ -58,6 +59,8 @@ class InSynth(declarations: List[Declaration], goalType: Type, ordered: Boolean
   
   def getCurrentBuilder = solver.currentBuilder
 
+  def getAllDeclarations = _declarations
+
 }
 
 object InSynth {
@@ -65,10 +68,7 @@ object InSynth {
   def apply(declarations: List[Declaration], goalType: Type, ordered: Boolean) =
     new InSynth(declarations, goalType, ordered)
   
-//  def apply(program: Program, hole: Hole, ordered: Boolean) =
-//    new InSynth(new LeonLoader(program, hole).load, hole.getType, ordered)
-    
-  def apply(loader: LeonLoader, ordered: Boolean) =
-    new InSynth(loader.load, loader.hole.getType, ordered)
+  def apply(loader: LeonLoader, goalType: Type, ordered: Boolean) =
+    new InSynth(loader.load, goalType, ordered)
   
 }
\ No newline at end of file
diff --git a/src/main/scala/insynth/InSynthTemp.scala b/src/main/scala/insynth/InSynthTemp.scala
deleted file mode 100644
index 8c06803df352eedf8f6cea6336c1e3999275831a..0000000000000000000000000000000000000000
--- a/src/main/scala/insynth/InSynthTemp.scala
+++ /dev/null
@@ -1,74 +0,0 @@
-package insynth
-
-import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
-import insynth.reconstruction.codegen.CodeGenerator
-import insynth.reconstruction.{ FastReconstructor => Reconstructor }
-
-import insynth.interfaces.Declaration
-import insynth.engine.InitialEnvironmentBuilder
-
-import insynth.leon.loader.LeonLoader
-import insynth.leon.LeonQueryBuilder
-
-import _root_.leon.purescala.Definitions.Program
-import _root_.leon.purescala.Trees.Hole
-import _root_.leon.purescala.TypeTrees.{ TypeTree => Type }
-
-import insynth.util.logging.HasLogger
-
-/**
- * Main class for the synthesis process invocation
- * @param program Leon program object that contains the hole
- * @param hole hole in the program on which the synthesis is called 
- */
-class InSynthTemp(declarations: List[Declaration], goalType: Type, ordered: Boolean = true) extends HasLogger {
-  
-//  def this(program: Program, hole: Hole, ordered: Boolean) =
-//    this(new LeonLoader(program, hole).load, hole.getType, ordered)
-    
-  def this(loader: LeonLoader, ordered: Boolean) =
-    this(loader.load, loader.hole.getType, ordered)
-  
-  lazy val solver = new Solver(declarations, new LeonQueryBuilder(goalType))
-  
-  def getExpressions = {
-    info("InSynth synthesizing type + " + goalType + " with declarations " + solver.allDeclarations.mkString("\n"))
-    val proofTree = solver.getProofTree
-    	
-		assert(proofTree != null, "Proof tree is null" )  
-    assert(1 == proofTree.getNodes.size)
-          
-    val codegen = new CodeGenerator
-    
-    Reconstructor(proofTree.getNodes.head, codegen, ordered)
-  }
-  
-  def getExpressions(builder: InitialEnvironmentBuilder) = {
-    info("InSynth synthesizing type + " + goalType + " with declarations " + builder.getAllDeclarations.mkString("\n"))
-    val proofTree = solver.getProofTree(builder)
-    info("Proof tree is acquired")
-    	
-		assert(proofTree != null, "Proof tree is null" )  
-    assert(1 == proofTree.getNodes.size)
-          
-    val codegen = new CodeGenerator
-    
-    Reconstructor(proofTree.getNodes.head, codegen, ordered)
-  }
-  
-  def getCurrentBuilder = solver.currentBuilder
-
-}
-
-object InSynthTemp {
-  
-  def apply(declarations: List[Declaration], goalType: Type, ordered: Boolean) =
-    new InSynthTemp(declarations, goalType, ordered)
-  
-//  def apply(program: Program, hole: Hole, ordered: Boolean) =
-//    new InSynthTemp(new LeonLoader(program, hole).load, hole.getType, ordered)
-    
-  def apply(loader: LeonLoader, ordered: Boolean) =
-    new InSynthTemp(loader.load, loader.hole.getType, ordered)
-  
-}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/DomainTypeTransformer.scala b/src/main/scala/insynth/leon/DomainTypeTransformer.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7c37f3322beaa68fdbb15bda390223884d6efbd5
--- /dev/null
+++ b/src/main/scala/insynth/leon/DomainTypeTransformer.scala
@@ -0,0 +1,56 @@
+package insynth.leon
+
+import insynth.structures._
+
+import leon.purescala.TypeTrees.{ TypeTree => LeonType, BottomType => LeonBottomType, _ }
+import leon.purescala.Common.FreshIdentifier
+import leon.purescala.Definitions._
+
+import scala.language.implicitConversions
+
+object DomainTypeTransformer extends ( LeonType => DomainType ) {
+  
+  val InSynthTypeTransformer = TypeTransformer
+  
+  def apply(typeDef: ClassTypeDef): DomainType = {    		
+		implicit def singletonList(x: DomainType) = List(x)
+
+    typeDef match {
+      case abs: AbstractClassDef => Atom(Const(abs.id.name))
+      case caseClassDef: CaseClassDef => Atom(Const(caseClassDef.id.name))
+    }
+  }
+	
+  def apply(leonType: LeonType): DomainType = {    		
+		implicit def singletonList(x: DomainType) = List(x)
+
+    leonType match {
+      case Untyped => throw new RuntimeException("Should not happen at this point")
+      case AnyType => Atom(Const("Any"))
+      case LeonBottomType => Atom(BottomType) //Atom(Const("Bottom"))
+      case BooleanType => Atom(Const("Boolean"))
+      case UnitType => Atom(Const("Unit"))
+      case Int32Type => Atom(Const("Int"))
+      case ListType(baseType) => Atom(InSynthTypeTransformer(leonType))
+      case ArrayType(baseType) => Atom(InSynthTypeTransformer(leonType))
+      case TupleType(baseTypes) => Atom(InSynthTypeTransformer(leonType))
+      case SetType(baseType) => Atom(InSynthTypeTransformer(leonType))
+      case MultisetType(baseType) => Atom(InSynthTypeTransformer(leonType))
+      case MapType(from, to) => Atom(InSynthTypeTransformer(leonType))
+      case FunctionType(froms, to) => transformFunction(to, froms)
+      case c: ClassType => Atom(Const(c.id.name))
+    }
+  }
+
+  private def transformFunction(fun: LeonType, params: List[LeonType]): DomainType = fun match {
+    case FunctionType(froms, to) =>
+      transformFunction(to, params ++ froms)
+    case Untyped => throw new RuntimeException("Should not happen at this point")
+    // query will have this
+    case LeonBottomType =>
+      Function( params map this, this(fun) )
+    case t =>
+      Function( params map this, this(t) )
+  }
+  
+}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/LeonDeclaration.scala b/src/main/scala/insynth/leon/LeonDeclaration.scala
index 5c263a3dd301e1f2a6513bfe2d7b9a05ae736dd5..229b18395916d8106a32c5e94447c8f2897c5c08 100644
--- a/src/main/scala/insynth/leon/LeonDeclaration.scala
+++ b/src/main/scala/insynth/leon/LeonDeclaration.scala
@@ -1,8 +1,8 @@
 package insynth.leon
 
 import insynth.structures.SuccinctType
-import insynth.interfaces.Declaration
 import insynth.structures.Weight._
+import insynth.load.Declaration
 
 import leon.purescala.TypeTrees.{ TypeTree => LeonType }
 import leon.purescala.Trees.Expr
@@ -12,7 +12,7 @@ case class LeonDeclaration(
 	val leonType: LeonType, val expression: ReconstructionExpression 
 )
 extends Declaration(inSynthType, weight) {
-      
+        
   def this(expression: ReconstructionExpression, inSynthType: SuccinctType,
     leonType: LeonType, commutative: Boolean, weight: Weight    
   ) = {
@@ -27,7 +27,7 @@ extends Declaration(inSynthType, weight) {
 	
   private var query = false
       
-  def getDomainType = leonType
+  def getDomainType = DomainTypeTransformer(leonType)
     
   def getSimpleName = expression.getSimpleName
   
diff --git a/src/main/scala/insynth/leon/LeonQuery.scala b/src/main/scala/insynth/leon/LeonQuery.scala
index c4e1dc70c55770a2f94f5ae9aa7649045c2ddbcd..9b4ba6d166c042f4da43a42a961815cfee94b2b5 100644
--- a/src/main/scala/insynth/leon/LeonQuery.scala
+++ b/src/main/scala/insynth/leon/LeonQuery.scala
@@ -3,7 +3,7 @@ package insynth.leon
 import insynth.leon.loader.DeclarationFactory
 import insynth.engine.InitialSender
 import insynth.structures.SuccinctType
-import insynth.interfaces.Query
+import insynth.query.Query
 
 import leon.purescala.TypeTrees._
 import leon.purescala.Common.FreshIdentifier
diff --git a/src/main/scala/insynth/leon/LeonQueryBuilder.scala b/src/main/scala/insynth/leon/LeonQueryBuilder.scala
index e8b63a103efa276d6c12a9bb38128c9474a5a11d..e78ef6e7b63056e07c8a8b23c668940c190c4bb6 100644
--- a/src/main/scala/insynth/leon/LeonQueryBuilder.scala
+++ b/src/main/scala/insynth/leon/LeonQueryBuilder.scala
@@ -1,9 +1,10 @@
 package insynth.leon
 
-import insynth.leon.loader.DeclarationFactory
-import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
+import insynth.query._
 import insynth.engine.InitialSender
-import insynth.interfaces.QueryBuilder
+import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
+
+import insynth.leon.loader.DeclarationFactory
 
 import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
 import leon.purescala.Common.FreshIdentifier
diff --git a/src/main/scala/insynth/leon/TypeTransformer.scala b/src/main/scala/insynth/leon/TypeTransformer.scala
index d8358f7d1386da17b96c740d327043a8c8e312ec..e22d48ba8123fcdba4c77d84ae0ac4d54bb5a89e 100644
--- a/src/main/scala/insynth/leon/TypeTransformer.scala
+++ b/src/main/scala/insynth/leon/TypeTransformer.scala
@@ -6,6 +6,10 @@ import leon.purescala.TypeTrees.{ TypeTree => LeonType, BottomType => LeonBottom
 import leon.purescala.Common.FreshIdentifier
 import leon.purescala.Definitions._
 
+// enable postfix operations and implicit conversions
+import scala.language.postfixOps
+import scala.language.implicitConversions
+
 object TypeTransformer extends ( LeonType => SuccinctType ) {
   
   def apply(typeDef: ClassTypeDef): SuccinctType = {    		
diff --git a/src/main/scala/insynth/leon/loader/HoleExtractor.scala b/src/main/scala/insynth/leon/loader/HoleExtractor.scala
deleted file mode 100644
index 61248d08b0f3aa093c9cb10053e67cf7ba88a2cb..0000000000000000000000000000000000000000
--- a/src/main/scala/insynth/leon/loader/HoleExtractor.scala
+++ /dev/null
@@ -1,103 +0,0 @@
-package insynth.leon.loader
-
-import insynth.leon.{ ImmediateExpression, LeonDeclaration }
-
-import leon.purescala.Definitions.{ Program, FunDef }
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.Common.{ Identifier }
-
-class HoleExtractor(program: Program, hole: Hole) {
-  
-  import DeclarationFactory._
-  
-  def extractHole: Option[(FunDef, List[LeonDeclaration])] = {
-    
-    // the list of declarations to be returned
-    //var list = scala.collection.mutable.MutableList[Declaration]()
-    
-    // XXX we currently go through all functions, not efficient!
-    var foundHoleCount = 0
-    for (
-      funDef <-program.definedFunctions;
-      if funDef.hasBody;
-      (foundHole, declarations) = scanMethod(funDef.getBody);      
-      if foundHole;
-      argDeclarations = funDef.args map { makeArgumentDeclaration(_) }
-    ) {
-      foundHoleCount+=1
-          	
-    	return Some((funDef, argDeclarations.toList ++ declarations))
-    }
-    //assert(foundHoleCount <= 1)
-    
-    None
-    
-  }
-  
-  def scanMethod(functionBody: Expr): (Boolean, Set[LeonDeclaration]) = {
-    
-    case class LocalPair(foundHole: Boolean, currentSet: Set[Identifier]) {
-    	def ++?(pair: Pair[Boolean, Set[Identifier]]): (Boolean, Set[Identifier]) = {
-    	  val (foundHoleSec, currentSetSec) = pair
-    	  if (foundHole)
-    	    (true, currentSet)
-    	  else (foundHoleSec, currentSet ++ currentSetSec)
-    	}  
-    	def +(id: Identifier): (Boolean, Set[Identifier]) = {
-    	  (foundHole, currentSet + id)
-    	}  
-    	def /:\(pair: Pair[Boolean, Set[Identifier]]): (Boolean, Set[Identifier]) = {
-    	  if (foundHole)
-    	    (foundHole, currentSet)
-  	    else
-  	      pair
-    	}  
-    }
-	  implicit def localPairCast(pair: Pair[Boolean, Set[Identifier]]) = LocalPair(pair._1, pair._2)
-    
-	  def allIdentifiers(expr: Expr) : (Boolean, Set[Identifier]) = expr match {
-	    case l @ Let(binder, e, b) => allIdentifiers(e) /:\ ( allIdentifiers(b) + binder )
-//	    case l @ LetVar(binder, e, b) => allIdentifiers(e) /:\ ( allIdentifiers(b) + binder )
-//	    case l @ LetDef(fd, b) =>
-//	      allIdentifiers(fd.getBody) /:\ ( allIdentifiers(b) + fd.id )
-	    
-	    //case block @ Block(exprs, last)	    
-	    // NOTE: NAryOperator covers block
-	    case n @ NAryOperator(args, _) =>
-	      ((false, Set[Identifier]()) /: (args map (allIdentifiers(_)))) {	        
-	        case (currentPair, newPair) => currentPair /:\ newPair
-	      }
-	    case b @ BinaryOperator(a1,a2,_) => allIdentifiers(a1) ++? allIdentifiers(a2)
-	    case u @ UnaryOperator(a,_) => allIdentifiers(a)
-	    case i @ IfExpr(a1,a2,a3) => allIdentifiers(a1) /:\ allIdentifiers(a2) /:\ allIdentifiers(a3)
-	    case m @ MatchExpr(scrut, cses) =>
-	      // ??
-	      allIdentifiers(scrut) ++?
-	      ( (false, Set[Identifier]()) /: ( cses map {
-	          cse =>
-	        	val rhsResult = allIdentifiers(cse.rhs)
-	        	(rhsResult._1, rhsResult._2 ++ cse.pattern.allIdentifiers)
-        	})
-        ) {        
-	        case (currentPair, newPair) => currentPair ++? newPair
-	      }
-	    case Variable(id) => (false, Set.empty)
-	    case h: Hole => (true, Set.empty) 
-	    case t: Terminal => (false, Set.empty)
-	  }
-	  
-	  val (foundHole, collectedIdentifiers) = allIdentifiers(functionBody)
-	  
-	  (
-      foundHole,
-		  for ( id <- collectedIdentifiers )
-		    yield makeDeclaration(
-	        ImmediateExpression( id, Variable(id) ), 
-	        id.getType
-	      )
-    )
-	  
-  }
-
-}
\ No newline at end of file
diff --git a/src/main/scala/insynth/leon/loader/Loader.scala b/src/main/scala/insynth/leon/loader/Loader.scala
index 47a6d517fabc7c5b4ac7739ac2b04ccca0d24a13..5a7a9080580ca02aa08f5d0987cd4467a5e56f93 100644
--- a/src/main/scala/insynth/leon/loader/Loader.scala
+++ b/src/main/scala/insynth/leon/loader/Loader.scala
@@ -2,17 +2,20 @@ package insynth.leon.loader
 
 import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
 import insynth.structures.{ SuccinctType => InSynthType }
-import insynth.interfaces.Loader
+import insynth.load.Loader
 import insynth.util.logging.HasLogger
 
 import leon.purescala.Definitions.{ Program, FunDef }
 import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
-import leon.purescala.Trees.{ Hole, Expr, FunctionInvocation, _ }
+import leon.purescala.Trees.{ Expr, FunctionInvocation, _ }
 import leon.purescala.Common.{ Identifier }
 import leon.purescala.Definitions.{ AbstractClassDef, CaseClassDef, ClassTypeDef }
 
-case class LeonLoader(program: Program, hole: Hole,
-  variables: List[Identifier], loadArithmeticOps: Boolean = true) extends Loader with HasLogger {  
+// enable postfix operations
+import scala.language.postfixOps
+
+case class LeonLoader(program: Program, variables: List[Identifier], loadArithmeticOps: Boolean = true)
+	extends Loader with HasLogger {  
   //var temporaryDesiredType: LeonType = Int32Type
   
   lazy val classMap: Map[Identifier, ClassType] = extractClasses
@@ -38,11 +41,11 @@ case class LeonLoader(program: Program, hole: Hole,
     /* add declarations to builder */
           
     // add function declarations
-    for( funDef@FunDef(id, returnType, args, _, _, _) <- program.definedFunctions ) {
-      val leonFunctionType = FunctionType(args map { _.tpe } toList, returnType)
+    for( funDef <- program.definedFunctions ) {
+      val leonFunctionType = FunctionType(funDef.args map { _.tpe } toList, funDef.returnType)
               
       val newDeclaration = makeDeclaration(
-        NaryReconstructionExpression( id, { args: List[Expr] => FunctionInvocation(funDef, args) } ), 
+        NaryReconstructionExpression( funDef.id, { args: List[Expr] => FunctionInvocation(funDef, args) } ), 
         leonFunctionType
       )        
       
@@ -78,17 +81,7 @@ case class LeonLoader(program: Program, hole: Hole,
       case _ =>
     }
     
-    list.toList
-    
-    // no need for doing this (we will have everything from the synthesis problem context)
-//    new HoleExtractor(program, hole).extractHole match {
-//      case Some((holeDef, decls)) =>
-//        list ++= decls
-//                  
-//        (list.toList, decls, holeDef)
-//      case _ =>
-//        throw new RuntimeException("Hole extractor problem")
-//    }     
+    list.toList   
   }
     
   def initializeSubclassesMap(program: Program) = {  
@@ -250,4 +243,4 @@ case class LeonLoader(program: Program, hole: Hole,
 //    assert(foundHoleCount <= 1)
 //    
 //    list toList
-//  }
\ No newline at end of file
+//  }
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/insynth/leon/loader/PreLoader.scala
index 8d420f8ad1980928f7760fd1093db65a77a77192..2a1d6fe0a9ea24395ae1f8f27d091c3d5443bc46 100644
--- a/src/main/scala/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/insynth/leon/loader/PreLoader.scala
@@ -9,6 +9,9 @@ import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
 import leon.purescala.Common.{ Identifier }
 import leon.purescala.Trees._
 
+// enable postfix operations
+import scala.language.postfixOps
+
 object PreLoader extends ( (Boolean) => List[Declaration] ) {
   
   import DeclarationFactory._
diff --git a/src/main/scala/insynth/reconstruction/FastReconstructor.scala b/src/main/scala/insynth/reconstruction/FastReconstructor.scala
deleted file mode 100644
index 72cba71ae22fedfdb6a60922f11ab5bee97e1218..0000000000000000000000000000000000000000
--- a/src/main/scala/insynth/reconstruction/FastReconstructor.scala
+++ /dev/null
@@ -1,47 +0,0 @@
-package insynth.reconstruction
-
-import insynth.structures.{ SimpleNode, Weight }
-import insynth.reconstruction.shortcut._
-import insynth.reconstruction.stream.{ Node => LambdaNode, _ }
-import insynth.reconstruction.codegen.CodeGenerator
-
-import insynth.Config
-import insynth.util.format.{ FormatSuccinctNode, FormatIntermediate, FormatStreamUtils }
-import insynth.util.logging.HasLogger
-import insynth.util._
-
-/**
- * Object for reconstruction of proof trees into output(s)
- */
-object FastReconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Output]) with HasLogger {
-
-  def apply(tree: SimpleNode, codeGenerator: CodeGenerator, streamOrdered: Boolean = false) = {		    
-    // logging
-    entering("apply", FormatSuccinctNode(tree, 8).toString)
-    fine("reconstructor got proof tree size: " + ProofTreeOperations.size(tree))
-         
-    // create an ordered/unordered extractor
-    val transformer = 
-      if (streamOrdered)
-        new Transformer2(new OrderedStreamFactory[LambdaNode])
-      else
-        new Transformer2(new UnorderedStreamFactory[LambdaNode])
-    
-    // transform the trees (first two steps of the code generation phase)
-    val extractedTrees = transformer(tree)
-    
-    // logging
-    info("extractor phase done")
-    
-    // for each tree, generate the code for it
-    val generatedCode = extractedTrees map {
-      resPair => Output(codeGenerator(resPair._1), resPair._2)
-    }
-        
-    // logging
-    info("solutions are generated")
-    
-    generatedCode
-  }
-  
-}
diff --git a/src/main/scala/insynth/reconstruction/Reconstructor.scala b/src/main/scala/insynth/reconstruction/Reconstructor.scala
index 858719a66f1c36adf43c835a5381b744f3e2c80a..a1e6506c1f73a5ec78abf9dd6c4cc79a8e8211c5 100644
--- a/src/main/scala/insynth/reconstruction/Reconstructor.scala
+++ b/src/main/scala/insynth/reconstruction/Reconstructor.scala
@@ -1,12 +1,11 @@
 package insynth.reconstruction
 
 import insynth.structures.{ SimpleNode, Weight }
-import insynth.reconstruction.intermediate.IntermediateTransformer
 import insynth.reconstruction.stream.{ Node => LambdaNode, _ }
+
 import insynth.reconstruction.codegen.CodeGenerator
 
-import insynth.Config
-import insynth.util.format.{ FormatSuccinctNode, FormatIntermediate, FormatStreamUtils }
+import insynth.util.format.{ FormatSuccinctNode, FormatStreamUtils }
 import insynth.util.logging.HasLogger
 import insynth.util._
 
@@ -16,39 +15,18 @@ import insynth.util._
 object Reconstructor extends ( (SimpleNode, CodeGenerator, Boolean) => Stream[Output]) with HasLogger {
 
   def apply(tree: SimpleNode, codeGenerator: CodeGenerator, streamOrdered: Boolean = false) = {		    
-    // logging
-    entering("apply", FormatSuccinctNode(tree, 8).toString)
-    fine("reconstructor got proof tree size: " + ProofTreeOperations.size(tree))
     
     // transform the trees (first two steps of the code generation phase)
-    val transformedTree = IntermediateTransformer(tree)
+    val stream = Streamer(tree, streamOrdered)
          
-    // logging
-    info("intermediate transform phase done")    
-    finest("after intermediate " + FormatIntermediate(transformedTree))
-    fine("intermediate tree size " + IntermediateTreeOperations.size(transformedTree))
-    
-    // create an ordered/unordered extractor
-    val extractor = 
-      if (streamOrdered)
-        new Extractor(new OrderedStreamFactory[LambdaNode])
-      else
-        new Extractor(new UnorderedStreamFactory[LambdaNode])
-                
-    // generate streams of lambda trees
-    val extractedTrees = extractor(transformedTree)
-    
-    // logging
-    info("extractor phase done")
-    finest("got streamable " + FormatStreamUtils(extractor.transformedStreamable))
+    info("streamer done, stream computed")
     
     // for each tree, generate the code for it
-    val generatedCode = extractedTrees map {
+    val generatedCode = stream map {
       resPair => Output(codeGenerator(resPair._1), resPair._2)
     }
         
-    // logging
-    info("solutions are generated")
+    info("stream of solutions is generated")
     
     generatedCode
   }
diff --git a/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala b/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
index 76663ae7a367113794e8bcaca204377e2daa9181..ae1f934415074fede778ba81279426f1a94eedda 100644
--- a/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
+++ b/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
@@ -3,18 +3,15 @@ package insynth.reconstruction.codegen
 import scala.text.Document
 import scala.text.Document.empty
 
-//import ch.epfl.insynth.reconstruction.intermediate._
-//import ch.epfl.insynth.trees
-//import ch.epfl.insynth.print._
-//import ch.epfl.insynth.reconstruction.combinator.{ NormalDeclaration, AbsDeclaration }
-import insynth.leon.{ LeonDeclaration => DomainDeclaration, _ }
+import insynth.leon._
 import insynth.reconstruction.stream._
 
-import insynth.util.format.{ FormatLeonType => FormatDomainType, FormatIntermediate }
+import insynth.structures.Function
+
 import insynth.util.logging.HasLogger
 
 import leon.purescala.Trees.{ Expr }
-import leon.purescala.TypeTrees.{ TypeTree => DomainType, FunctionType => Function }
+import leon.purescala.TypeTrees.{ TypeTree => DomainType, FunctionType }
 import leon.purescala.{ TypeTrees => domain }
 import leon.purescala.Trees.{ Expr => CodeGenOutput }
 
@@ -33,7 +30,7 @@ class CodeGenerator extends (Node => CodeGenOutput) with HasLogger {
   def apply(tree: Node) = {
     // match the starting tree to an application that produces query type
     tree match {
-      case Application(domain.FunctionType(_, _ /* BottomType */), queryDec :: List(innerApp)) =>
+      case Application(Function(_, _ /* BottomType */), queryDec :: List(innerApp)) =>
       	transform(innerApp)
       case _ => throw new RuntimeException
     }
@@ -61,13 +58,13 @@ class CodeGenerator extends (Node => CodeGenOutput) with HasLogger {
         // what to do here
         throw new RuntimeException
       // identifier from the scope
-      case Identifier(tpe, DomainDeclaration(_, _, _, im: ImmediateExpression)) => 
+      case Identifier(tpe, LeonDeclaration(_, _, _, im: ImmediateExpression)) => 
         im()
       // apply parameters in the tail of params according to the head of params 
       case app@Application(tpe, params) => {        
         // match the application definition term
         params.head match {
-          case Identifier(_, decl)  => {            
+          case Identifier(_, decl: LeonDeclaration)  => {            
 	          info("Generating application: " + decl + " with params: " + params + " params.size = " + params.size)   
 
 	          // for an expression of each parameters yield the appropriate transformed expression	            
@@ -93,17 +90,17 @@ class CodeGenerator extends (Node => CodeGenOutput) with HasLogger {
                 fun(paramsExpr.head)
                 
               // this should not happen
-              case _ => throw new RuntimeException
+              case _ => throw new Exception("Unsupported reconstruction: " + decl.expression)
             }
           } // case Identifier
           
-          case innerApp@Application(appType: domain.FunctionType, params) =>
-            warning("cannot have app head: " + innerApp + " in application " + app)
-          	throw new RuntimeException
+          case innerApp@Application(appType: Function, params) =>
+            warning("Cannot have app head: " + innerApp + " in application " + app)
+          	throw new Exception("Cannot have app head: " + innerApp + " in application " + app)
                       
           // function that is created as an argument or anything else
           case /*Identifier(_, _:AbsDeclaration) | */_:Variable | _ =>
-          	throw new RuntimeException
+          	throw new Exception("Unsupported combination for application head " + params.head)
           	
         } // params.head match 
       }
diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc6c37c7dbe3d4ba7b58ec77d5dead0b165a9e76
--- /dev/null
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -0,0 +1,81 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+
+class StopwatchCollection(name: String) {
+  var acc: Long = 0L
+  
+  var stopwatches = List[Stopwatch]()
+
+  def +=(sw: Stopwatch) = synchronized { acc += sw.getMillis }
+
+  def getMillis = {
+    val running =
+	    (0L /: stopwatches) {
+	      (res, sw) => res + sw.getMillis
+	    }
+      
+    acc + running
+  }
+  
+  def newStopwatch = {
+    val result = new Stopwatch()
+    stopwatches :+= result
+    result
+  }
+
+  override def toString = "%20s: %5dms".format(name, acc)
+}
+
+/** Implements a stopwatch for profiling purposes */
+class Stopwatch(name: String = "Stopwatch") {
+  var beginning: Long = 0L
+  var end: Long = 0L
+  var acc: Long = 0L
+
+  def start: this.type = {
+    beginning = System.currentTimeMillis
+    end       = 0L
+    this
+  }
+
+  def stop {
+    end        = System.currentTimeMillis
+    acc       += (end - beginning)
+    beginning  = 0L
+  }
+
+  def getMillis: Long = {
+    if (isRunning) {
+      acc + (System.currentTimeMillis-beginning)
+    } else {
+      acc
+    }
+  }
+    
+  def profile[T](block: => T): T = {
+    if (isRunning) stop
+    
+    start
+    val result = block    // call-by-name
+    stop
+    
+    result
+  }
+
+  def isRunning = beginning != 0L
+
+  override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "")
+}
+
+object StopwatchCollections {
+  private var all = Map[String, StopwatchCollection]()
+
+  def get(name: String): StopwatchCollection = all.getOrElse(name, {
+    val sw = new StopwatchCollection(name)
+    all += name -> sw
+    sw
+  })
+
+  def getAll = all
+}
diff --git a/src/main/scala/leon/codegen/CodeGenEvalParams.scala b/src/main/scala/leon/codegen/CodeGenEvalParams.scala
new file mode 100644
index 0000000000000000000000000000000000000000..31f8c49df55d54acb48ed4d60d2c14f083c16df7
--- /dev/null
+++ b/src/main/scala/leon/codegen/CodeGenEvalParams.scala
@@ -0,0 +1,7 @@
+package leon
+package codegen
+
+case class CodeGenEvalParams (
+  maxFunctionInvocations: Int = -1,
+  checkContracts: Boolean = false
+)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 551ea44c0d05e18f1dc004b1df93e4987e0f8746..2b914a9716811ca60542d3d520e91b8f88740a90 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -313,6 +313,14 @@ class PrettyPrinter(sb: StringBuffer = new StringBuffer) {
     case MultisetType(bt) => sb.append("Multiset["); pp(bt, lvl); sb.append("]")
     case TupleType(tpes) => ppNaryType(tpes, "(", ", ", ")", lvl)
     case c: ClassType => sb.append(c.classDef.id)
+    case FunctionType(fts, tt) => {
+      if (fts.size > 1)
+        ppNaryType(fts, "(", ", ", ")", lvl)
+      else if (fts.size == 1)
+        pp(fts.head, lvl)
+      sb.append(" => ")
+      pp(tt, lvl)
+    }
     case _ => sb.append("Type?")
   }
 
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 0c338c4259bbb121ad4b70a6c833fe418767dacc..67241adeffd6adebee90741c3db3835983cb1f00 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -325,6 +325,14 @@ class ScalaPrinter(sb: StringBuffer = new StringBuffer) extends PrettyPrinter(sb
       pp(bt, lvl)
       sb.append("]")
     case TupleType(tpes) => ppNaryType(tpes, "(", ", ", ")", lvl)
+    case FunctionType(fts, tt) =>
+      if (fts.size > 1) {
+        ppNaryType(fts, "(", ", ", ")", lvl)
+      } else if (fts.size == 1) {
+        pp(fts.head, lvl)
+      }
+      sb.append(" => ")
+      pp(tt, lvl)
     case c: ClassType => sb.append(c.classDef.id)
     case _ => sb.append("Type?")
   }
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 96265cf88c6736dbba11b6337c6cde901838d14f..74b35aeb6c34ebc631c22aeb692960ad5a83ba39 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -155,6 +155,16 @@ object TypeTrees {
       case (_,InfiniteSize) => InfiniteSize
       case (FiniteSize(n),FiniteSize(m)) => FiniteSize(scala.math.pow(m+1, n).toInt)
     }
+    case FunctionType(fts, tt) => {
+      val fromSizes = fts map domainSize
+      val toSize = domainSize(tt)
+      if (fromSizes.exists(_ == InfiniteSize) || toSize == InfiniteSize)
+        InfiniteSize
+      else {
+        val n = toSize.asInstanceOf[FiniteSize].size
+        FiniteSize(scala.math.pow(n, fromSizes.foldLeft(1)((acc, s) => acc * s.asInstanceOf[FiniteSize].size)).toInt)
+      }
+    }
     case c: ClassType => InfiniteSize
   }
 
@@ -205,6 +215,7 @@ object TypeTrees {
   case class SetType(base: TypeTree) extends TypeTree
   case class MultisetType(base: TypeTree) extends TypeTree
   case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
+  case class FunctionType(from: List[TypeTree], to: TypeTree) extends TypeTree
   case class ArrayType(base: TypeTree) extends TypeTree
 
   sealed abstract class ClassType extends TypeTree {
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/lesynth/SynthesizerExamples.scala
index ddcd81a59b7a777fe499ec28e2391fa3fbb52205..a66557c4ddcdb473bb24112666df2c8b1a81efd8 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/lesynth/SynthesizerExamples.scala
@@ -4,7 +4,7 @@ import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
 import scala.collection.mutable.{ PriorityQueue, ArrayBuffer, HashSet }
 import scala.util.control.Breaks._
 
-import leon.{ Reporter, DefaultReporter, SilentReporter, LeonContext }
+import leon.{ Reporter, DefaultReporter, LeonContext }
 import leon.Main.processOptions
 
 import leon.solvers._
@@ -20,10 +20,9 @@ import leon.evaluators.EvaluationResults
 import leon.evaluators._
 import leon.synthesis.{ Problem, SynthesisContext }
 
-import insynth.interfaces.Declaration
 import insynth.{ Solver => _, _ }
 import insynth.leon.loader._
-import insynth.leon._
+import insynth.leon.{ LeonDeclaration => Declaration, _ }
 import insynth.engine._
 import insynth.reconstruction.Output
 import insynth.util.logging.HasLogger
@@ -36,10 +35,12 @@ import lesynth.refinement._
 import SynthesisInfo._
 import SynthesisInfo.Action._
 
+// enable postfix operations
+import scala.language.postfixOps
+
 class SynthesizerForRuleExamples(
   // some synthesis instance information
-  val mainSolver: Solver,
-  var solver: IncrementalSolver,
+  val mainSolver: SolverFactory[Solver],
   val program: Program,
   val desiredType: LeonType,
   val holeFunDef: FunDef,
@@ -52,7 +53,7 @@ class SynthesizerForRuleExamples(
 //  leonTimeout: Int = 1, // seconds
   analyzeSynthesizedFunctionOnly: Boolean = false,
   showLeonOutput: Boolean = false,
-  reporter: Reporter = new DefaultReporter,
+  reporter: Reporter,
   //examples: List[Map[Identifier, Expr]] = Nil,
   // we need the holeDef to know the right ids
   introduceExamples: (() => List[Map[Identifier, Expr]]) = { () => Nil },
@@ -76,9 +77,8 @@ class SynthesizerForRuleExamples(
   
   // objects used in the synthesis
   private var loader: LeonLoader = _
-  private var inSynth: InSynthTemp = _
-  private var inSynthBoolean: InSynthTemp = _
-  private var hole: Hole = _
+  private var inSynth: InSynth = _
+  private var inSynthBoolean: InSynth = _
   // initial declarations
   private var allDeclarations: List[Declaration] = _
 
@@ -108,7 +108,7 @@ class SynthesizerForRuleExamples(
   // information about the synthesis
   private val synthInfo = new SynthesisInfo
   
-  val verifier = new RelaxedVerifier(solver, problem, synthInfo)
+  val verifier = new RelaxedVerifier(mainSolver, problem, synthInfo)
   import verifier._
 
   def synthesize: Report = {
@@ -128,7 +128,7 @@ class SynthesizerForRuleExamples(
     var keepGoing = true
     // update flag in case of time limit overdue
     def checkTimeout =
-      if (synthesisContext.shouldStop.get) {
+      if (synthesisContext.context.interruptManager.isInterrupted()) {
         reporter.info("Timeout occured, stopping this synthesis rules")
         keepGoing = false
         true
@@ -379,16 +379,15 @@ class SynthesizerForRuleExamples(
 
   def initialize = {
     // create new insynth object
-    hole = Hole(desiredType)
-    loader = new LeonLoader(program, hole, problem.as, false)
-    inSynth = new InSynthTemp(loader, true)
+    loader = new LeonLoader(program, problem.as, false)
+    inSynth = new InSynth(loader, desiredType, true)
     // save all declarations seen
-    allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
+    allDeclarations = inSynth.declarations
     // make conditions synthesizer
-    inSynthBoolean = new InSynthTemp(allDeclarations, BooleanType, true)
+    inSynthBoolean = new InSynth(allDeclarations, BooleanType, true)
 
     // funDef of the hole
-    fine("postcondition is: " + holeFunDef.getPostcondition)
+    fine("postcondition is: " + holeFunDef.postcondition.get)
     fine("declarations we see: " + allDeclarations.map(_.toString).mkString("\n"))
     //    interactivePause
 
@@ -396,7 +395,7 @@ class SynthesizerForRuleExamples(
     accumulatingCondition = BooleanLiteral(true)
     // save initial precondition
     initialPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
-    val holeFunDefBody = holeFunDef.getBody
+    val holeFunDefBody = holeFunDef.body.get
     // accumulate the final expression of the hole
     accumulatingExpression = (finalExp: Expr) => {      
 	    def replaceChoose(expr: Expr) = expr match {
@@ -427,7 +426,7 @@ class SynthesizerForRuleExamples(
   def tryToSynthesizeBranch(snippetTree: Expr, examplesPartition: (Seq[Example], Seq[Example])): Boolean = {
     val (succeededExamples, failedExamples) = examplesPartition
     // replace hole in the body with the whole if-then-else structure, with current snippet tree
-    val oldBody = holeFunDef.getBody
+    val oldBody = holeFunDef.body.get
     val newBody = accumulatingExpression(snippetTree)
     holeFunDef.body = Some(newBody)
 
@@ -435,7 +434,7 @@ class SynthesizerForRuleExamples(
     val oldPrecondition = holeFunDef.precondition.getOrElse(BooleanLiteral(true))
     holeFunDef.precondition = Some(initialPrecondition)
 
-    snippetTree.setType(hole.desiredType)
+    snippetTree.setType(desiredType)
     //holeFunDef.getBody.setType(hole.desiredType)
     reporter.info("Current candidate solution is:\n" + holeFunDef)
 
@@ -586,10 +585,12 @@ class SynthesizerForRuleExamples(
 				    assert(newBody.getType != Untyped)
             val resFresh2 = FreshIdentifier("result22", true).setType(newBody.getType)
 				
+              val (id, post) = newFun.postcondition.get
+
               val newCandidate = 
 				    Let(resFresh2, newBody,
-				      matchToIfThenElse(replace(Map(ResultVariable() -> LeonVariable(resFresh2)),
-				        newFun.getPostcondition)))
+				      matchToIfThenElse(replace(Map(LeonVariable(id) -> LeonVariable(resFresh2)),
+				        post)))
 				    finest("New fun for Error evaluation: " + newFun)
 //				    println("new candidate: " + newBody)
 	
@@ -597,8 +598,8 @@ class SynthesizerForRuleExamples(
 			          program.mainObject.copy(defs = newFun +: program.mainObject.defs ))
 //				    println("new program: " + newProgram)
 			          
-		          val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram,		              
-		              _root_.leon.codegen.CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true))
+		          val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram		              
+		              /* TODO:, _root_.leon.codegen.CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true) */)
 	
 				    	val res = _evaluator.eval(newCandidate, exMapping)
 				    	println(res)
@@ -654,10 +655,12 @@ class SynthesizerForRuleExamples(
 				    assert(newBody.getType != Untyped)
             val resFresh2 = FreshIdentifier("result22", true).setType(newBody.getType)
 				
+              val (id, post) = newFun.postcondition.get
+
               val newCandidate = 
 				    Let(resFresh2, newBody,
-				      matchToIfThenElse(replace(Map(ResultVariable() -> LeonVariable(resFresh2)),
-				        newFun.getPostcondition)))
+				      matchToIfThenElse(replace(Map(LeonVariable(id) -> LeonVariable(resFresh2)),
+				        post)))
 				    finest("New fun for Error evaluation: " + newFun)
 //				    println("new candidate: " + newBody)
 	
@@ -665,8 +668,8 @@ class SynthesizerForRuleExamples(
 			          program.mainObject.copy(defs = newFun +: program.mainObject.defs ))
 //				    println("new program: " + newProgram)
 			          
-		          val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram,		              
-		              _root_.leon.codegen.CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true))
+		          val _evaluator = new CodeGenEvaluator(synthesisContext.context, newProgram /* TODO: ,		              
+		              _root_.leon.codegen.CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true) */)
 	
 				    	val res = _evaluator.eval(newCandidate, exMapping)
 				    	println("for mapping: " + exMapping + "res is: " + res)
@@ -754,4 +757,4 @@ class SynthesizerForRuleExamples(
   }
 
 }
-	
\ No newline at end of file
+	
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
index e6560d3beaf9900dc64e288e97d887eacae7e384..a24e93558751b8149cbdeb7bed959b37703cd085 100644
--- a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
@@ -23,10 +23,10 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
 
   private var _examples = ArrayBuffer(transformExamples(inputExamples): _*)
 
-  val evaluationContext = ctx.copy(reporter = new SilentReporter)
+  val evaluationContext = ctx
   
   fine("building codegen evaluator with program:\n" + program)
-  lazy val _evaluator = new CodeGenEvaluator(evaluationContext, program, params)
+  lazy val _evaluator = new CodeGenEvaluator(evaluationContext, program/*TODO:, params*/)
   override def getEvaluator = _evaluator
   
   def transformExamples(examples: Seq[Example]) =
@@ -133,4 +133,4 @@ case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
     (passed.size, passed map (_._2))
   }
 
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala b/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
index c9b13a86649182f0fbcf795df56b5b9fd6572250..45a22e5582c94fc211bbcb2aa68d3f85c960be13 100644
--- a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
+++ b/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
@@ -27,7 +27,7 @@ case class DefaultExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
     _examples ++= newExamples.map(_.map)
   }
 
-  val evaluationContext = ctx.copy(reporter = new SilentReporter)
+  val evaluationContext = ctx
   
   lazy val _evaluator = new DefaultEvaluator(evaluationContext, program)
   override def getEvaluator = _evaluator
@@ -85,4 +85,4 @@ case class DefaultExampleRunner(program: Program, funDef: FunDef, ctx: LeonConte
     (passed.size, passed)
   }
 
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/examples/InputExamples.scala b/src/main/scala/lesynth/examples/InputExamples.scala
index 106442bbc164993164b0a1dcf12a71a1b30e1c0d..9336f53373dbe3cd2f5b802acc3850d5e78d75e3 100755
--- a/src/main/scala/lesynth/examples/InputExamples.scala
+++ b/src/main/scala/lesynth/examples/InputExamples.scala
@@ -10,7 +10,7 @@ import leon.evaluators.Evaluator
 import leon.synthesis.Problem
 import leon.LeonContext
 
-import insynth.leon.loader.{ HoleExtractor, LeonLoader }
+import insynth.leon.loader.LeonLoader
 import leon.datagen._
 
 object InputExamples {
@@ -49,12 +49,12 @@ object InputExamples {
     )
   }
 
-  def getFixedInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader) = {
+  def getFixedInputExamples(argumentIds: Seq[Identifier], loader: LeonLoader, goalType: TypeTree) = {
     argumentIds match {
       case singleArgument :: Nil if isList(singleArgument) =>
         introduceOneListArgumentExamples(argumentIds, loader)
       case first :: second :: Nil if isList(first) && isList(second) =>
-        introduceTwoListArgumentsExamples(argumentIds, loader)
+        introduceTwoListArgumentsExamples(argumentIds, loader, goalType)
       case first :: second :: Nil if isInt(first) && isList(second) =>
         introduceExamplesIntList(argumentIds, loader)
       case _ => null
@@ -119,9 +119,10 @@ object InputExamples {
       yield Map(argumentIds(0) -> list)
   }
 
-  def introduceTwoListArgumentsExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader) = {
+  def introduceTwoListArgumentsExamples(argumentIds: Seq[leon.purescala.Common.Identifier], loader: LeonLoader,
+  	goalType: TypeTree) = {
 
-    loader.hole.getType match {
+    goalType match {
       case ct: ClassType =>
         val setSubclasses = loader.directSubclassesMap(ct).map(_.asInstanceOf[CaseClassType].classDef)
 
diff --git a/src/main/scala/lesynth/ranking/Candidate.scala b/src/main/scala/lesynth/ranking/Candidate.scala
index 3305b1832e2d4ccb9df515a79950d456ad041981..761a0e2b3a5148e9601f4878115805338b9d7e1d 100644
--- a/src/main/scala/lesynth/ranking/Candidate.scala
+++ b/src/main/scala/lesynth/ranking/Candidate.scala
@@ -18,7 +18,7 @@ object Candidate {
   def getFreshResultVariable(tpe: TypeTree) = _freshResultVariable = FreshIdentifier("result", true).setType(tpe)
   
   def makeDefaultCandidates(candidatePairs: IndexedSeq[Output], bodyBuilder: Expr => Expr, funDef: FunDef) = {
-    getFreshResultVariable(funDef.getBody.getType)
+    getFreshResultVariable(funDef.body.get.getType)
     candidatePairs map {
       pair =>
       	DefaultCandidate(pair.getSnippet, bodyBuilder(pair.getSnippet), pair.getWeight, funDef)
@@ -26,7 +26,7 @@ object Candidate {
   }
   
   def makeCodeGenCandidates(candidatePairs: IndexedSeq[Output], bodyBuilder: Expr => Expr, funDef: FunDef) = {
-    getFreshResultVariable(funDef.getBody.getType)
+    getFreshResultVariable(funDef.body.get.getType)
     candidatePairs map {
       pair =>
       	CodeGenCandidate(pair.getSnippet, bodyBuilder(pair.getSnippet), pair.getWeight, funDef)
@@ -54,10 +54,12 @@ case class DefaultCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, holeFunD
     assert(bodyExpr.getType != Untyped)
     val resFresh = freshResultVariable//.setType(expr.getType)
 
+    val (id, post) = holeFunDef.postcondition.get
+
     // body can contain (self-)recursive calls
     Let(resFresh, bodyExpr,
-      replace(Map(ResultVariable() -> Variable(resFresh)),
-        matchToIfThenElse(holeFunDef.getPostcondition)))
+      replace(Map(Variable(id) -> Variable(resFresh)),
+        matchToIfThenElse(post)))
   }
   
   override def prepareExpression = {
@@ -96,10 +98,12 @@ case class CodeGenCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, holeFunD
     assert(bodyExpr.getType != Untyped)
     val resFresh = freshResultVariable//.setType(expr.getType)
 
+    val (id, post) = newFun.postcondition.get
+
     // body can contain (self-)recursive calls
     (Let(resFresh, newBody,
-      replace(Map(ResultVariable() -> Variable(resFresh)),
-        matchToIfThenElse(newFun.getPostcondition)))
+      replace(Map(Variable(id) -> Variable(resFresh)),
+        matchToIfThenElse(post)))
     ,
     newFun)
   }
@@ -109,4 +113,4 @@ case class CodeGenCandidate(expr: Expr, bodyExpr: Expr, weight: Weight, holeFunD
 //    finest("going to evaluate candidate for: " + expressionToEvaluate)
     expressionToEvaluate
   }
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/ranking/Ranker.scala b/src/main/scala/lesynth/ranking/Ranker.scala
index ebf6d42970ece8a984c38299c29274a1c33175a4..39c4f753aeaaa58f80a0056aae3a03be8dde0695 100644
--- a/src/main/scala/lesynth/ranking/Ranker.scala
+++ b/src/main/scala/lesynth/ranking/Ranker.scala
@@ -6,6 +6,9 @@ import scala.collection._
 
 import leon.purescala.Trees.{ Variable => LeonVariable, _ }
 
+// enable postfix
+import scala.language.postfixOps
+
 class Ranker(candidates: IndexedSeq[Candidate], evaluation: Evaluation, checkTimeout: (() => Boolean) = { () => false }, printStep: Boolean = false) {
   
   val candidatesSize = candidates.size
diff --git a/src/main/scala/lesynth/refinement/VariableRefiner.scala b/src/main/scala/lesynth/refinement/VariableRefiner.scala
index a980e6fd98a215a6d5b7a2f960a0cd691d62ddb0..df821f62fad976b6b2461f1e0d21ab18a9b3afda 100755
--- a/src/main/scala/lesynth/refinement/VariableRefiner.scala
+++ b/src/main/scala/lesynth/refinement/VariableRefiner.scala
@@ -10,22 +10,21 @@ import leon.purescala.TypeTrees._
 import leon.purescala.Definitions._
 import leon.purescala.Common.{ Identifier, FreshIdentifier }
 
-import insynth.interfaces._
 import insynth.leon.loader._
-import insynth.leon._
+import insynth.leon.{ LeonDeclaration => Declaration, _ }
 
 import insynth.util.logging.HasLogger
 
 // each variable of super type can actually have a subtype
 // get sine declaration maps to be able to refine them  
-class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[LeonDeclaration],
-  classMap: Map[Identifier, ClassType], reporter: Reporter = new SilentReporter) extends HasLogger {  
+class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[Declaration],
+  classMap: Map[Identifier, ClassType], reporter: Reporter) extends HasLogger {  
   
     // map from identifier into a set of possible subclasses
   protected var variableRefinements: MutableMap[Identifier, MutableSet[ClassType]] = MutableMap.empty
     for (varDec <- variableDeclarations) {
       varDec match {
-        case LeonDeclaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, Variable(id))) =>
+        case Declaration(_, _, typeOfVar: ClassType, ImmediateExpression(_, Variable(id))) =>
           variableRefinements += (id -> MutableSet(directSubclassMap(typeOfVar).toList: _*))
         case _ =>
       }
@@ -73,13 +72,13 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
   def refinedDeclarations(id: Identifier, newType: ClassType, allDeclarations: List[Declaration]) =
     for (dec <- allDeclarations)
       yield dec match {
-        case LeonDeclaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>	              
+        case Declaration(inSynthType, _, decClassType, imex @ ImmediateExpression(_, Variable(`id`))) =>	              
 	        ((
             newType.classDef match {
               case newTypeCaseClassDef@CaseClassDef(_, parent, fields) =>
                 fine("matched case class def for refinement " + newTypeCaseClassDef)
 		            for (field <- fields)
-				          yield LeonDeclaration(
+				          yield Declaration(
 						        ImmediateExpression(id.name + "." + field.id.name,
 					            CaseClassSelector(newTypeCaseClassDef, imex.expr, field.id) ), 
 						        TypeTransformer(field.id.getType), field.id.getType
@@ -87,9 +86,9 @@ class VariableRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variabl
               case _ =>
                 Seq.empty
             }
-	        ): Seq[Declaration]) :+ LeonDeclaration(imex, TypeTransformer(newType), newType)
+	        ): Seq[Declaration]) :+ Declaration(imex, TypeTransformer(newType), newType)
         case _ =>
           Seq(dec)
       }
   
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala b/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
index 0ffe1aa469cb50e8ac917752801ffccad66ef220..59ec68fcc9167c2bd6c2a878585b1286f59ec5ce 100755
--- a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
+++ b/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
@@ -14,7 +14,6 @@ import leon.solvers._
 import leon.purescala.Common.{ Identifier, FreshIdentifier }
 import leon.synthesis.Problem
 
-import insynth.interfaces._
 import insynth.leon.loader._
 import insynth.leon._
 
@@ -23,13 +22,15 @@ import insynth.util.logging.HasLogger
 // each variable of super type can actually have a subtype
 // get sine declaration maps to be able to refine them  
 class VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], variableDeclarations: Seq[LeonDeclaration],
-  classMap: Map[Identifier, ClassType], solver: Solver, reporter: Reporter = new SilentReporter)
+  classMap: Map[Identifier, ClassType], solverf: SolverFactory[Solver], reporter: Reporter)
   extends VariableRefiner(directSubclassMap, variableDeclarations, classMap, reporter) with HasLogger {  
+
+  val solver = SimpleSolverAPI(solverf)
     
-  override def checkRefinements(expr: Expr, condition: Expr, allDeclarations: List[Declaration]) = {
+  override def checkRefinements(expr: Expr, condition: Expr, allDeclarations: List[LeonDeclaration]) = {
     val superResult = super.checkRefinements(expr, condition, allDeclarations)
     if (superResult._1 == false) {
-	    val variables = allIdentifiers(expr)
+	    val variables = variablesOf(expr)
 	    if (variables.size == 1) {
 	      val variable = variables.head
 	      variable match {
@@ -83,7 +84,7 @@ class VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], v
     else superResult
   } 
   
-  def refineProblem(p: Problem, solver: Solver) = {
+  def refineProblem(p: Problem) = {
 
     val newAs = p.as.map {
       case oldId@IsTyped(id, AbstractClassType(cd)) =>
@@ -125,4 +126,4 @@ class VariableSolverRefiner(directSubclassMap: Map[ClassType, Set[ClassType]], v
   }
 
   
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
index 05a6a4cd10397e9770b011936718dd7d23076187..95324fce673698bb056e3f5769b4dadcc995e1b5 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -8,7 +8,7 @@ import leon.purescala.TreeOps._
 import leon.purescala.Extractors._
 import leon.purescala.Definitions._
 import leon.synthesis._
-import leon.solvers.{ Solver, TimeoutSolver }
+import leon.solvers._
 import leon.evaluators.CodeGenEvaluator
 
 import lesynth.examples.InputExamples._
@@ -16,7 +16,7 @@ import lesynth.evaluation._
 
 import leon.StopwatchCollections
 
-case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") with TopLevelRule {
+case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abduction synthesis (two phase).") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
 
     p.xs match {
@@ -24,7 +24,7 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
         List(new RuleInstantiation(p, this, SolutionBuilder.none, "Condition abduction") {
           def apply(sctx: SynthesisContext): RuleApplicationResult = {
             try {
-              val solver = new TimeoutSolver(sctx.solver, 500L)
+              val solver = sctx.solverFactory.withTimeout(500L)
               val program = sctx.program
               val reporter = sctx.reporter
 
@@ -51,11 +51,10 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
                 
             	val evaluationStrategy = new CodeGenEvaluationStrategy(program, holeFunDef, sctx.context, 5000)
                 	
-                holeFunDef.postcondition = Some(replace(
-                  Map(givenVariable.toVariable -> ResultVariable().setType(holeFunDef.returnType)), p.phi))
+                holeFunDef.postcondition = Some((givenVariable, p.phi))
 
                 val synthesizer = new SynthesizerForRuleExamples(
-                  solver, solver.getNewSolver, program, desiredType, holeFunDef, p, sctx, evaluationStrategy,
+                  solver, program, desiredType, holeFunDef, p, sctx, evaluationStrategy,
                   20, 1, 
                   reporter = reporter,
                   introduceExamples = getInputExamples,  
@@ -69,8 +68,8 @@ case object ConditionAbductionSynthesisTwoPhase extends Rule("Condition abductio
                     println(fr.summaryString)
                     println("Compilation time: " + StopwatchCollections.get("Compilation").getMillis)
                     RuleSuccess(
-                      Solution(BooleanLiteral(true), Set.empty, Tuple(Seq(resFunDef.body.get)),
-                    		isTrusted = !synthesizer.verifier.isTimeoutUsed)
+                      Solution(BooleanLiteral(true), Set.empty, Tuple(Seq(resFunDef.body.get))),
+                    		isTrusted = !synthesizer.verifier.isTimeoutUsed
                     )
                 }
               } catch {
diff --git a/src/main/scala/lesynth/verification/AbstractVerifier.scala b/src/main/scala/lesynth/verification/AbstractVerifier.scala
index 18e4875d57f7b80ecbd4c303d82f61caf26c5878..0508293bbca94c0fb86e6eabb4b4b607175a7b12 100644
--- a/src/main/scala/lesynth/verification/AbstractVerifier.scala
+++ b/src/main/scala/lesynth/verification/AbstractVerifier.scala
@@ -11,10 +11,12 @@ import leon.synthesis._
 
 import insynth.util.logging._
 
-abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
+abstract class AbstractVerifier(solverf: SolverFactory[Solver], p: Problem,
   synthInfo: SynthesisInfo)
 	extends HasLogger {
     
+  val solver = solverf.getNewSolver
+
   import SynthesisInfo.Action._
   
   def analyzeFunction(funDef: FunDef) = {
@@ -22,7 +24,7 @@ abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
     fine("Analyzing function: " + funDef)
 
     // create an expression to verify
-    val theExpr = generateInductiveVerificationCondition(funDef, funDef.getBody)
+    val theExpr = generateInductiveVerificationCondition(funDef, funDef.body.get)
      
     solver.push
     val valid = checkValidity(theExpr)
@@ -58,7 +60,7 @@ abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
     case class Replacement(id: Identifier, exprReplaced: FunctionInvocation) {
       def getMapping: Map[Expr, Expr] = {
         val funDef = exprReplaced.funDef
-        val pairList = (ResultVariable(), id.toVariable) ::
+        val pairList = (Variable(funDef.postcondition.get._1), id.toVariable) ::
         	(funDef.args.map(_.toVariable).toList zip exprReplaced.args)
       	pairList.toMap
       }
@@ -82,16 +84,17 @@ abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
        
     // build the verification condition
     val resFresh = FreshIdentifier("result", true).setType(newBody.getType)
-    val bodyAndPost = 		    
+    val (id, post) = funDef.postcondition.get
+    val bodyAndPost =
 	    Let(
     		resFresh, newBody,
-    		replace(Map(ResultVariable() -> resFresh.toVariable), matchToIfThenElse(funDef.getPostcondition))
+    		replace(Map(Variable(id) -> resFresh.toVariable), matchToIfThenElse(post))
   		)	
 
 		val precondition = if( isThereARecursiveCall ) {
-		  And( funDef.getPrecondition :: replacements.map( r => replace(r.getMapping, funDef.getPostcondition)) )
+		  And( funDef.precondition.get :: replacements.map( r => replace(r.getMapping, post)) )
 		} else
-		  funDef.getPrecondition
+		  funDef.precondition.get
 //    val bodyAndPost = 		    
 //	    Let(
 //    		resFresh, newBody,
@@ -116,4 +119,4 @@ abstract class AbstractVerifier(solver: IncrementalSolver, p: Problem,
   
   def checkSatisfiabilityNoMod(expression: Expr): Boolean
   
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/verification/RelaxedVerifier.scala b/src/main/scala/lesynth/verification/RelaxedVerifier.scala
index 07393f990a123d03fb6345eb99b653b9153cc5d7..91d8b09466ab19ce58232e30ec90044b92ee19e3 100644
--- a/src/main/scala/lesynth/verification/RelaxedVerifier.scala
+++ b/src/main/scala/lesynth/verification/RelaxedVerifier.scala
@@ -11,8 +11,8 @@ import leon.synthesis._
 
 import insynth.util.logging._
 
-class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
-	extends AbstractVerifier(solver, p, synthInfo) with HasLogger {
+class RelaxedVerifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
+	extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
   
   var _isTimeoutUsed = false
   
@@ -72,4 +72,4 @@ class RelaxedVerifier(solver: IncrementalSolver, p: Problem, synthInfo: Synthesi
     }
   }
   
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/lesynth/verification/Verifier.scala b/src/main/scala/lesynth/verification/Verifier.scala
index f21277c7c4800ba475d188fcd63539e9baa21f74..eda23f3f2abae1c32887503a194bcf3a9e69cfe0 100644
--- a/src/main/scala/lesynth/verification/Verifier.scala
+++ b/src/main/scala/lesynth/verification/Verifier.scala
@@ -11,8 +11,8 @@ import leon.synthesis._
 
 import insynth.util.logging._
 
-class Verifier(solver: IncrementalSolver, p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
-	extends AbstractVerifier(solver, p, synthInfo) with HasLogger {
+class Verifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
+	extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
     
   import SynthesisInfo.Action._
   
@@ -65,4 +65,4 @@ class Verifier(solver: IncrementalSolver, p: Problem, synthInfo: SynthesisInfo =
     }
   }
   
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/insynth/InSynthTempTest.scala b/src/test/scala/insynth/InSynthTempTest.scala
deleted file mode 100644
index 61f1d467ec5c9c63d6309b14b696d88f00889b65..0000000000000000000000000000000000000000
--- a/src/test/scala/insynth/InSynthTempTest.scala
+++ /dev/null
@@ -1,673 +0,0 @@
-package insynth
-
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
-
-import insynth.reconstruction.{ intermediate => int }
-import insynth.reconstruction.{ stream => lambda }
-import insynth.reconstruction.shortcut._
-import insynth.reconstruction.stream.{ OrderedStreamFactory }
-import insynth.reconstruction.codegen._
-import insynth.reconstruction.Output
-
-import _root_.leon.purescala.Definitions._
-import _root_.leon.purescala.Common._
-import _root_.leon.purescala.TypeTrees._
-import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
-
-import lesynth.refinement._
-import lesynth.examples._
-import lesynth.evaluation.CodeGenEvaluationStrategy
-import lesynth.ranking.Candidate
-
-import org.junit.{ Test, Ignore }
-import org.junit.Assert._
-
-import insynth.util.format._
-import insynth.util._
-import lesynth.util._
-
-import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
-
-// TODO test abstractions (vals)
-class InSynthTempTest {
-
-  import CommonDeclarations._
-  import CommonProofTrees._
-  import CommonLambda._
-  import DeclarationFactory._
-  
-  import Scaffold._
-  import TestConfig._
-  
-	import ProofTreeOperations.StringNode
-    
-  val transformer = new Transformer2(new OrderedStreamFactory)
-  val codegen = new CodeGenerator
-  
-  val maxElToOutput = 20
-  
-  import lambda.Node._
-  
-  def assertWeight(lambdaNode: lambda.Node, weight: Float) =
-    assertEquals(size(lambdaNode), weight, 0f)
-    
-  def assertWeight(expected: Int, weight: Float) =
-    assertEquals(expected.toFloat, weight, 0f)	
-    
-  def assertWeight(pair: (lambda.Node, Float)) =
-    assertEquals("Node " + pair._1, size(pair._1), pair._2, 0f)	    
-    
-  def assertTake(stream: Stream[(lambda.Node, Float)], num: Int) = {
-    val result = stream take num
-    val message = "Part of the resulting stream: " + result.take(maxElToOutput).mkString("\n")
-    
-    for (ind <- 0 until result.size)
-      assertWeight(result(ind))
-    for (ind <- 0 until result.size - 1)
-      assertTrue("Weight are not in non-decreasing order.\n" + "At position " + ind + "\n" + message, stream(ind)._2 <= stream(ind + 1)._2)
-    result
-  }
-  
-  def interactivePause = {    
-    System.out.println("Press Any Key To Continue...");
-    new java.util.Scanner(System.in).nextLine();
-  }
-      
-  @Ignore
-  def testAddresses: Unit = {  
-  	
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      assertEquals(1, problem.xs.size)
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-	    val solver = inSynth.solver	    
-	    val solution = solver.getProofTree
-	    
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("AddressBook", Set(
-            StringNode("[Cons=>List]", Set(StringNode("Cons")))
-            ,
-            StringNode("pers", Set(StringNode("makeAddressBook")))
-          ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToPers", Set(
-          StringNode("makeAddressBook", Set(
-//        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("Address", Set( ))
-        ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToBusiness", Set(
-          StringNode("makeAddressBook", Set(
-//        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("Address", Set( ))
-        ))
-      ))
-      
-      val extractorResults = assertTake(transformer(solution.getNodes.head), 1000)
-	          
-//      val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
-//        (resMap, pair) =>
-//          val snippet = codegen(pair._1)
-//          resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
-//      }
-      
-//      val resTemp = transformer(solution.getNodes.head).take(100)
-//      
-//      println(resTemp.head)
-//      val it = resTemp.iterator.buffered
-//      println(it.head)
-//      println(it.hasNext)
-//      println(it.head)
-//      println(it.hasNext)
-//      
-//      for (output <- extractorResults) {
-//      	print("%20s %5f" format (output._1, output._2))
-//      	
-//		    System.out.println("Press Any Key To Continue...");
-//		    new java.util.Scanner(System.in).nextLine();
-//      }
-//      println("\nExtracted: " + extractorResults.size)
-       	
-      val message = 
-        (for (output <- extractorResults)
-        	yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
-      assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
-      assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
-//      
-//      println("Duplicity map size " + duplicityMap.size)
-//      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
-//        println("Key: " + key)
-//        println("Values: " + value.mkString("\n"))        
-//      }
-    }
-  }
- 
-  @Ignore
-  def testAddressesWithRefinement: Unit = {  
-  	
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      assertEquals(1, problem.xs.size)
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
-        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
-	    println(declsMessage)      
-      
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-      
-	    val solver = inSynth.solver	    
-	    val solution = solver.getProofTree(builder)
-      
-      val extractorResults = assertTake(transformer(solution.getNodes.head), 1000)
-	          
-//      val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
-//        (resMap, pair) =>
-//          val snippet = codegen(pair._1)
-//          resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
-//      }
-      
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("AddressBook", Set(
-            StringNode("[Cons=>List]", Set(StringNode("Cons")))
-            ,
-            StringNode("pers", Set(StringNode("makeAddressBook")))
-          ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToPers", Set(
-          StringNode("makeAddressBook", Set(
-        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("a", Set( ))
-        ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToBusiness", Set(
-          StringNode("makeAddressBook", Set(
-        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("a", Set( ))
-        ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToBusiness", Set(
-          StringNode("makeAddressBook", Set(
-        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("l.a", Set( ))
-        ))
-      ))
-//      val resTemp = transformer(solution.getNodes.head).take(100)
-//      
-//      println(resTemp.head)
-//      val it = resTemp.iterator.buffered
-//      println(it.head)
-//      println(it.hasNext)
-//      println(it.head)
-//      println(it.hasNext)
-//      
-//      for (output <- extractorResults) {
-//      	print("%20s %5f" format (output._1, output._2))
-//      	
-//		    System.out.println("Press Any Key To Continue...");
-//		    new java.util.Scanner(System.in).nextLine();
-//      }
-//      println("\nExtracted: " + resTemp.size)
-//    	println("\nExtracted: " + extractorResults.size)
-       	
-      val message = 
-        (for (output <- extractorResults)
-        	yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
-      assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
-      assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
-//      
-//      println("Duplicity map size " + duplicityMap.size)
-//      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
-//        println("Key: " + key)
-//        println("Values: " + value.mkString("\n"))        
-//      }
-    }
-  } 
- 
-  @Ignore
-  def testAddressesWithRefinementCodeGen: Unit = {  
-  	
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      assertEquals(1, problem.xs.size)
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
-        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
-	    println(declsMessage)      
-      
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-      
-	    val solver = inSynth.solver	    
-	    val solution = solver.getProofTree(builder)
-      
-      val extractorResults = assertTake(transformer(solution.getNodes.head), 20000)
-	          
-      var ind = 1
-      for ((output, snippet) <- extractorResults zip (extractorResults map { p => codegen(p._1) })) {
-      	print("%20s %20s\n".format(snippet, output._1.toString))
-      	ind +=1     	
-      	
-      	if ((ind % 1000) == 0) {
-      	  interactivePause
-      	}
-      }
-       	
-      val message = 
-        (for (output <- extractorResults)
-        	yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
-      assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
-      assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
-//      
-//      println("Duplicity map size " + duplicityMap.size)
-//      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
-//        println("Key: " + key)
-//        println("Values: " + value.mkString("\n"))        
-//      }
-    }
-  } 
-  
-  @Ignore
-  def testAddressesWithRefinementTime: Unit = {  
-  	
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      assertEquals(1, problem.xs.size)
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
-        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
-      
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-      
-	    val solver = inSynth.solver	    
-	    val solution = solver.getProofTree(builder)
-      
-	    val startTime = System.currentTimeMillis
-      val extractorResults = assertTake(transformer(solution.getNodes.head), 5000)
-      println("Time for extracting 5000 solutions: " + (System.currentTimeMillis - startTime))
-	          
-//      val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
-//        (resMap, pair) =>
-//          val snippet = codegen(pair._1)
-//          resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
-//      }
-      
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("AddressBook", Set(
-            StringNode("[Cons=>List]", Set(StringNode("Cons")))
-            ,
-            StringNode("pers", Set(StringNode("makeAddressBook")))
-          ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToPers", Set(
-          StringNode("makeAddressBook", Set(
-        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("a", Set( ))
-        ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToBusiness", Set(
-          StringNode("makeAddressBook", Set(
-        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("a", Set( ))
-        ))
-      ))
-	    assertTrue(
-		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-        ProofTreeOperations.checkInhabitants(solution,
-        StringNode("addToBusiness", Set(
-          StringNode("makeAddressBook", Set(
-        		StringNode("l.tail", Set())
-          ))
-          , 
-          StringNode("l.a", Set( ))
-        ))
-      ))
-//      val resTemp = transformer(solution.getNodes.head).take(100)
-//      
-//      println(resTemp.head)
-//      val it = resTemp.iterator.buffered
-//      println(it.head)
-//      println(it.hasNext)
-//      println(it.head)
-//      println(it.hasNext)
-//      
-//      for (output <- extractorResults) {
-//      	print("%20s %5f" format (output._1, output._2))
-//      	
-//		    System.out.println("Press Any Key To Continue...");
-//		    new java.util.Scanner(System.in).nextLine();
-//      }
-//      println("\nExtracted: " + resTemp.size)
-//    	println("\nExtracted: " + extractorResults.size)
-       	
-      val message = 
-        (for (output <- extractorResults)
-        	yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
-      assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
-      assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
-//      
-//      println("Duplicity map size " + duplicityMap.size)
-//      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
-//        println("Key: " + key)
-//        println("Values: " + value.mkString("\n"))        
-//      }
-    }
-  } 
- 
-  @Ignore
-  def testListConcatWithRefinementCodeGen: Unit = {  
-  	
-    for ((sctx, funDef, problem) <- forFile(lesynthSynthesisDir + "List/ListConcat.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      assertEquals(1, problem.xs.size)
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
-        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.tail"))
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.head"))
-	    println(declsMessage)      
-      
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-      
-	    val solver = inSynth.solver	    
-	    val solution = solver.getProofTree(builder)
-      
-      val extractorResults = assertTake(transformer(solution.getNodes.head), 1000)
-	          
-      var ind = 1
-      for ((output, snippet) <- extractorResults zip (extractorResults map { p => codegen(p._1) })) {
-      	print("%20s %20s\n".format(snippet, output._1.toString))
-      	ind +=1     	
-      	
-      	if ((ind % 1000) == 0) {
-      	  interactivePause
-      	}
-      }
-       	
-//      val message = 
-//        (for (output <- extractorResults)
-//        	yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
-//      assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
-//      assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
-//      
-//      println("Duplicity map size " + duplicityMap.size)
-//      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
-//        println("Key: " + key)
-//        println("Values: " + value.mkString("\n"))        
-//      }
-    }
-  } 
-  
-  @Test
-  def testAddressesWithRefinementBoolean: Unit = {  
-  	
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      assertEquals(1, problem.xs.size)
-      val resultVariable = problem.xs.head
-      val hole = Hole(BooleanType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
-        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail"))
-      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
-	    println(declsMessage)      
-      
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-      
-	    val solver = inSynth.solver	    
-	    val solution = solver.getProofTree(builder)
-      
-      val extractorResults = assertTake(transformer(solution.getNodes.head), 100)
-	          
-//      val duplicityMap = (Map[Expr, Set[(lambda.Node, Float)]]() /: extractorResults) {
-//        (resMap, pair) =>
-//          val snippet = codegen(pair._1)
-//          resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
-//      }
-      
-//	    assertTrue(
-//		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-//        ProofTreeOperations.checkInhabitants(solution,
-//        StringNode("AddressBook", Set(
-//            StringNode("[Cons=>List]", Set(StringNode("Cons")))
-//            ,
-//            StringNode("pers", Set(StringNode("makeAddressBook")))
-//          ))
-//      ))
-//	    assertTrue(
-//		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-//        ProofTreeOperations.checkInhabitants(solution,
-//        StringNode("addToPers", Set(
-//          StringNode("makeAddressBook", Set(
-//        		StringNode("l.tail", Set())
-//          ))
-//          , 
-//          StringNode("a", Set( ))
-//        ))
-//      ))
-//	    assertTrue(
-//		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-//        ProofTreeOperations.checkInhabitants(solution,
-//        StringNode("addToBusiness", Set(
-//          StringNode("makeAddressBook", Set(
-//        		StringNode("l.tail", Set())
-//          ))
-//          , 
-//          StringNode("a", Set( ))
-//        ))
-//      ))
-//	    assertTrue(
-//		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
-//        ProofTreeOperations.checkInhabitants(solution,
-//        StringNode("addToBusiness", Set(
-//          StringNode("makeAddressBook", Set(
-//        		StringNode("l.tail", Set())
-//          ))
-//          , 
-//          StringNode("l.a", Set( ))
-//        ))
-//      ))
-//      val resTemp = transformer(solution.getNodes.head).take(100)
-//      
-//      println(resTemp.head)
-//      val it = resTemp.iterator.buffered
-//      println(it.head)
-//      println(it.hasNext)
-//      println(it.head)
-//      println(it.hasNext)
-//      
-      for (output <- extractorResults) {
-      	print("%20s %5f" format (output._1, output._2))
-      	
-		    System.out.println("Press Any Key To Continue...");
-		    new java.util.Scanner(System.in).nextLine();
-      }
-//      println("\nExtracted: " + resTemp.size)
-//    	println("\nExtracted: " + extractorResults.size)
-       	
-//      val message = 
-//        (for (output <- extractorResults)
-//        	yield "%20s %5f" format (output._1, output._2)).mkString("\n") + "\nExtracted: " + extractorResults.size
-//      assertTrue("addToPers not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToPers"))
-//      assertTrue("addToBusiness not found in extracted. results:\n" + message, extractorResults.exists(_._1.toString contains "addToBusiness"))
-//      
-//      println("Duplicity map size " + duplicityMap.size)
-//      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) {
-//        println("Key: " + key)
-//        println("Values: " + value.mkString("\n"))        
-//      }
-    }
-  } 
- 
-
-}
\ No newline at end of file
diff --git a/src/test/scala/insynth/InSynthTest.scala b/src/test/scala/insynth/InSynthTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..acf730adf28b246711457e9642eeefed463ea8f8
--- /dev/null
+++ b/src/test/scala/insynth/InSynthTest.scala
@@ -0,0 +1,302 @@
+package insynth
+
+import insynth.leon._
+import insynth.leon.loader._
+import insynth.engine._
+
+import insynth.reconstruction._
+import insynth.reconstruction.{ stream => lambda }
+import insynth.reconstruction.stream.{ OrderedStreamFactory }
+import insynth.reconstruction.codegen._
+import insynth.reconstruction.Output
+
+import _root_.leon.purescala.Definitions._
+import _root_.leon.purescala.Common._
+import _root_.leon.purescala.TypeTrees._
+import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
+
+//import lesynth.refinement._
+//import lesynth.examples._
+//import lesynth.evaluation.CodeGenEvaluationStrategy
+//import lesynth.ranking.Candidate
+
+import org.junit.{ Test, Ignore }
+import org.junit.Assert._
+import org.scalatest.junit.JUnitSuite
+
+import insynth.util.format._
+import insynth.util._
+
+import _root_.util._
+
+import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
+
+// TODO test abstractions (vals)
+class InSynthTest extends JUnitSuite {
+
+  import CommonDeclarations._
+  import CommonProofTrees._
+  import CommonLambda._
+  import DeclarationFactory._
+  
+  import Scaffold._
+  
+	import ProofTreeOperations.StringNode
+
+	val insynthTestDir = "testcases/condabd/test/insynth/" 
+    
+  val transformer = Streamer.apply _
+  val codegen = (new CodeGenerator).apply _
+  
+  val maxElToOutput = 20
+  
+  import lambda.Node._
+  
+  def assertWeight(lambdaNode: lambda.Node, weight: Float) =
+    assertEquals(size(lambdaNode), weight, 0f)
+    
+  def assertWeight(expected: Int, weight: Float) =
+    assertEquals(expected.toFloat, weight, 0f)	
+    
+  def assertWeight(pair: (lambda.Node, Float)) =
+    assertEquals("Node " + pair._1, size(pair._1), pair._2, 0f)	    
+    
+  def assertTake(stream: Stream[(lambda.Node, Float)], num: Int) = {
+    val result = stream take num
+    def message(pos: Int) = "Part of the resulting stream: " + result.slice(pos - 10, pos + 10).mkString("\n")
+    
+    for (ind <- 0 until result.size)
+      assertWeight(result(ind))
+    for (ind <- 0 until result.size - 1)
+      assertTrue("Weights are not in non-decreasing order.\n" + "At position " + ind + "\n" + message(ind), stream(ind)._2 <= stream(ind + 1)._2)
+    result
+  }
+
+  def assertNoDuplicity(extractorResults: Stream[(lambda.Node, Float)]) = {    
+    // note that duplicates may exist in generated code (e.g. because coercions), but should not before that
+    val duplicityMap = (Map[lambda.Node, Set[(lambda.Node, Float)]]() /: extractorResults) {
+      (resMap, pair) =>
+        val snippet = pair._1
+        resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
+    }
+          
+    lazy val duplicityMessage = 
+      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) yield
+        ("Key: " + key) + ("\nValues: " + value.mkString("\n"))        
+      
+    assertTrue(
+      "There are some duplications in generated code:\n" + duplicityMessage,
+      duplicityMap.filter(_._2.size > 1).isEmpty
+    )    
+  }
+  
+  def interactivePause = {    
+    System.out.println("Press Any Key To Continue...");
+    new java.util.Scanner(System.in).nextLine();
+  }
+      
+  @Test
+  def testAddressesProofTree {  
+  	
+    for ((sctx, funDef, problem) <- forFile(insynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader, resultVariable.getType, true)
+	    val solver = inSynth.solver	    
+	    val solution = solver.getProofTree
+	    
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("AddressBook", Set(
+            StringNode("[Cons=>List]", Set(StringNode("Cons")))
+            ,
+            StringNode("pers", Set(StringNode("makeAddressBook")))
+          ))
+      ))
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("addToPers", Set(
+          StringNode("makeAddressBook", Set())
+          , 
+          StringNode("Address", Set( ))
+        ))
+      ))
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("addToBusiness", Set(
+          StringNode("makeAddressBook", Set())
+          , 
+          StringNode("Address", Set( ))
+        ))
+      ))
+    }
+  }
+      
+  @Test
+  def testAddressesExpressionsTypeAddress {  
+      	
+    for ((sctx, funDef, problem) <- forFile(insynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader, resultVariable.getType, true)
+	    val solver = inSynth.solver	    
+	    val solution = solver.getProofTree
+
+      val extractorResults = assertTake(transformer(solution.getNodes.head, true), 1000)
+      assertNoDuplicity(extractorResults)
+	          
+      val extractedSnipptes = extractorResults map { pair => codegen(pair._1) }
+      
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    "AddressBook(Nil, l)",
+  	    "makeAddressBook(l)"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+
+			assertTrue(
+		    extractedSnipptes.exists(_.toString contains "addToPers")
+	    )
+			assertTrue(
+		    extractedSnipptes.exists(_.toString contains "addToBusiness")
+	    )
+      
+    }
+  }
+  
+  @Ignore("See this weight bug in InSynth")
+  @Test
+  def testAddressesExpressionsTypeBoolean {  
+      	
+    for ((sctx, funDef, problem) <- forFile(insynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader, BooleanType, true)
+	    val solver = inSynth.solver	    
+	    val solution = solver.getProofTree
+
+      val extractorResults = assertTake(transformer(solution.getNodes.head, true), 1000)
+      assertNoDuplicity(extractorResults)
+      
+      val extractedSnipptes = extractorResults map { pair => codegen(pair._1) }
+      
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    "allPrivate(AddressBook(Nil, l))",
+  	    "allBusiness(makeAddressBook(l))",
+  	    "allBusiness(makeAddressBook(l)) && allPrivate(AddressBook(Nil, l))"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+    }
+  }
+
+  @Test
+  def testAddressesExpressionsTypeAddressWithAddition {  
+      	
+    for ((sctx, funDef, problem) <- forFile(insynthTestDir + "AddressesWithAddition.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      // note problem.as does not contain function arguments, thus we use funDef.args
+      //val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, arguments.toList, false)
+	    val inSynth = new InSynth(loader.load, resultVariable.getType, true)
+	    val solver = inSynth.solver	    
+	    val solution = solver.getProofTree
+	          
+      val extractedSnipptes = inSynth.getExpressions.map(_.getSnippet) take 1000
+      
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    "AddressBook(Nil, l)",
+  	    "makeAddressBook(l, x, y)",
+  	    "addToPers(AddressBook(l, l), Address(x, x, y))",
+  	    "addToBusiness(AddressBook(l, l), Address(x, x, y))"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+      
+    }
+  }
+
+  @Test
+  def testDeclarations {  
+      	
+    for ((sctx, funDef, problem) <- forFile(insynthTestDir + "AddressesWithAddition.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      // note problem.as does not contain function arguments, thus we use funDef.args
+      //val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, arguments.toList, false)
+	    val inSynth = new InSynth(loader.load, resultVariable.getType, true)
+	          
+      val allDeclarations = inSynth.getAllDeclarations.map(d => (d.getSimpleName, d.leonType.toString)).toSet
+
+      val expectedDeclarations = Set(
+        ("AddressBook", "(List, List) => AddressBook"),
+        ("[Cons=>List]", "Cons => List"),
+        ("pers", "AddressBook => List"),
+        ("addToPers", "(AddressBook, Address) => AddressBook"),
+        ("addToBusiness", "(AddressBook, Address) => AddressBook"),
+        ("l", "List"),
+        ("tail", "Cons => List"),
+        ("a", "Cons => Address"),
+        ("x", "Int"),
+        ("y", "Boolean")
+  		)
+  		
+		  assertTrue(
+	      "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
+	      expectedDeclarations.subsetOf(allDeclarations)	      
+      )
+    }
+  }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/loader/LoaderTest.scala b/src/test/scala/insynth/loader/LoaderTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5982957f78f699a20b46b529d307c8a2c322c4de
--- /dev/null
+++ b/src/test/scala/insynth/loader/LoaderTest.scala
@@ -0,0 +1,130 @@
+package insynth
+package loader
+
+import _root_.util._
+
+import insynth.leon._
+import insynth.leon.loader._
+
+import _root_.leon.purescala.Definitions._
+import _root_.leon.purescala.Common._
+import _root_.leon.purescala.TypeTrees._
+import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
+
+import org.junit.{ Test, Ignore }
+import org.junit.Assert._
+import org.scalatest.junit.JUnitSuite
+
+class LoaderTest extends JUnitSuite {
+
+  import Scaffold._
+
+	val insynthTestDir = "testcases/condabd/test"
+  val testDir = insynthTestDir + "/insynth/"
+    
+  @Test
+  def testAddresses {
+    val fileName = testDir + "Addresses.scala"
+  	
+    for ((sctx, funDef, problem) <- forFile(fileName)) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    
+      val allDeclarations = loader.load.map(d => (d.getSimpleName, d.leonType.toString)).toSet
+
+      val expectedDeclarations = Set(
+        ("AddressBook", "(List, List) => AddressBook"),
+        ("[Cons=>List]", "Cons => List"),
+        ("pers", "AddressBook => List"),
+        ("makeAddressBook", "List => AddressBook"),
+        ("addToPers", "(AddressBook, Address) => AddressBook"),
+        ("addToBusiness", "(AddressBook, Address) => AddressBook"),
+        ("l", "List"),
+        ("tail", "Cons => List"),
+        ("a", "Cons => Address")
+  		)
+  		
+		  assertTrue(
+	      "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
+	      expectedDeclarations.subsetOf(allDeclarations)	      
+      )
+    }
+  }
+ 
+  @Test
+  def testListConcat {
+    val fileName = testDir + "ListConcat.scala"
+  	
+    for ((sctx, funDef, problem) <- forFile(fileName)) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    
+      val allDeclarations = loader.load.map(d => (d.getSimpleName, d.leonType.toString)).toSet
+
+      val expectedDeclarations = Set(
+        ("[Nil=>List]", "Nil => List"),
+        ("[Cons=>List]", "Cons => List"),
+        ("concat", "(List, List) => List"),
+        ("l1", "List"),
+        ("l2", "List"),
+        ("tail", "Cons => List"),
+        ("head", "Cons => Int")
+  		)
+  		
+		  assertTrue(
+	      "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
+	      expectedDeclarations.subsetOf(allDeclarations)	      
+      )
+    }
+  } 
+  
+  @Test
+  def testAddressesWithAddition {
+    val fileName = testDir + "AddressesWithAddition.scala"
+  	
+    for ((sctx, funDef, problem) <- forFile(fileName)) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = funDef.args.map(_.id).toList //problem.as)
+      assertTrue(varsInScope.size >= 3)
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    
+      val allDeclarations = loader.load.map(d => (d.getSimpleName, d.leonType.toString)).toSet
+
+      val expectedDeclarations = Set(
+        ("AddressBook", "(List, List) => AddressBook"),
+        ("[Cons=>List]", "Cons => List"),
+        ("pers", "AddressBook => List"),
+        ("addToPers", "(AddressBook, Address) => AddressBook"),
+        ("addToBusiness", "(AddressBook, Address) => AddressBook"),
+        ("l", "List"),
+        ("tail", "Cons => List"),
+        ("a", "Cons => Address"),
+        ("x", "Int"),
+        ("y", "Boolean")
+  		)
+  		
+		  assertTrue(
+	      "Expected:\n" + expectedDeclarations.mkString("\n") + "\nFound:\n" + allDeclarations.mkString("\n"),
+	      expectedDeclarations.subsetOf(allDeclarations)	      
+      )
+    }
+  } 
+
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala b/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
index c9b7c528bccc728c92b3dd891afed2b8136cd1aa..3d86a6fd81a32564f59cb9d6c26b491f64971509 100644
--- a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
+++ b/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
@@ -2,6 +2,7 @@ package insynth.reconstruction
 
 import org.junit.Assert._
 import org.junit.{ Test, Ignore }
+import org.scalatest.junit.JUnitSuite
 
 import insynth.reconstruction.codegen.CodeGenerator
 
@@ -11,7 +12,7 @@ import insynth.testutil.{ CommonLambda, CommonDeclarations }
 
 // NOTE function cannot return function in Leon, no need to test that
 
-class CodeGeneratorTest {
+class CodeGeneratorTest extends JUnitSuite {
     
   import CommonLambda._
   import CommonDeclarations._
@@ -53,11 +54,6 @@ class CodeGeneratorTest {
     assertTrue(twoLevCase1 + " not found. " + message, generated contains twoLevCase1)
     assertTrue(twoLevCase2 + " not found. " + message, generated contains twoLevCase2)
         
-//    val threeLevCase1 = FunctionInvocation(threeParFunctionDef, List(oneLevCase1, twoLevCase2, BooleanLiteral(false)))
-//    val threeLevCase2 = FunctionInvocation(threeParFunctionDef, List(twoLevCase2, threeLevCase1, BooleanLiteral(false)))
-//    
-//    assertTrue(threeLevCase1 + " not found. " + message, generated contains threeLevCase1)
-//    assertTrue(threeLevCase2 + " not found. " + message, generated contains threeLevCase2)
   }
   
 }
\ No newline at end of file
diff --git a/src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala b/src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala
deleted file mode 100644
index 46a41a1a1c7954c836fea8f4e8b5675dc7f216a8..0000000000000000000000000000000000000000
--- a/src/test/scala/insynth/reconstruction/PhaseCombinationTest.scala
+++ /dev/null
@@ -1,74 +0,0 @@
-package insynth.reconstruction
-
-import org.junit.{ Test, Ignore }
-import org.junit.Assert._
-
-import insynth.reconstruction.intermediate.IntermediateTransformer
-import insynth.reconstruction.stream.{ Extractor, UnorderedStreamFactory }
-import insynth.reconstruction.codegen.CodeGenerator
-
-import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
-import leon.purescala.Common.{ FreshIdentifier }
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees.{ Variable => LeonVariable, _ }
-
-import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonIntermediate, CommonLambda, CommonLeonExpressions }
-
-class PhaseCombinationTest {
-
-  import CommonDeclarations._
-  import CommonProofTrees._
-  import CommonIntermediate._
-  import CommonLambda._
-  import CommonLeonExpressions._
-      
-  @Test
-  def treeBoolToInt {
-    val (queryNode, query) = exampleBoolToInt
-    
-    val intermediateTree = IntermediateTransformer(queryNode)
-        
-    val codeGenerator = new CodeGenerator
-    
-    val extractor = new Extractor(new UnorderedStreamFactory)
-    
-    val extractorResults = extractor(intermediateTree) take 1
-    
-    assertEquals(1, extractorResults.size)
-    
-    val codeGenResult = codeGenerator(extractorResults.head._1)
-    
-    assertEquals(FunctionInvocation(functionBoolToIntFunDef, List(BooleanLiteral(false))), codeGenResult)    
-  }
-  
-  @Test
-  def treeIntToIntBoth {
-    val queryNode = exampleIntToIntBoth
-    
-    val intermediateTree = IntermediateTransformer(queryNode)
-    
-    assertEquals(constructIntToIntIntermediateBoth, intermediateTree)
-            
-    val extractor = new Extractor(new UnorderedStreamFactory)
-    
-    val extractorResults = (extractor(intermediateTree) take (5 * 2 * 2)) map { _._1 }	    
-    
-    assertEquals(5 * 4, extractorResults.size)	    	  
-    
-    for (node <- constructIntAndBoolToIntIntermediateLambda(5))
-    	assertTrue(node + " is not extracted.", extractorResults contains node)
-    
-    val codeGenerator = new CodeGenerator
-    
-    val expressions = extractorResults.map(codeGenerator(_)).toSet
-    
-    assertTrue(expressions contains boolInv)
-    assertTrue(expressions contains inv1WithBoolInv)
-    assertTrue(expressions contains inv1WithInt)
-    assertTrue(expressions contains inv2WithInt)
-    assertTrue(expressions contains inv3WithInt)  
-    assertTrue(expressions contains inv2WithBoolInv)    
-    assertTrue(expressions contains inv3WithBoolInv)      
-  }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala b/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
index 1c1f6b5df18c3d10253074f663e000a786123312..177f2e01e61a82f6ead2e71a696c02d0c2747335 100644
--- a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
+++ b/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
@@ -2,9 +2,9 @@ package insynth.reconstruction
 
 import org.junit.{ Test, Ignore, BeforeClass, AfterClass }
 import org.junit.Assert._
+import org.scalatest.junit.JUnitSuite
 
 import insynth.reconstruction.codegen.CodeGenerator
-import insynth.Config
 
 import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
 import leon.purescala.Common.{ FreshIdentifier }
@@ -13,7 +13,7 @@ import leon.purescala.Trees.{ Variable => LeonVariable, _ }
 
 import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLeonExpressions, CommonUtils }
 
-class ReconstructorTest {
+class ReconstructorTest extends JUnitSuite {
 
   import CommonDeclarations._
   import CommonProofTrees._
@@ -44,13 +44,14 @@ class ReconstructorTest {
     
     val expressions = expStream.map(_.snippet).take(20).toSet
     
-    assertTrue(expressions contains boolInv)
-    assertTrue(expressions contains inv1WithBoolInv)
+    assertTrue(expressions contains inv1boolInv)
+    assertTrue(expressions contains inv2WithBoolInv)
     assertTrue(expressions contains inv1WithInt)
     assertTrue(expressions contains inv2WithInt)
     assertTrue(expressions contains inv3WithInt)  
-    assertTrue(expressions contains inv2WithBoolInv)    
-    assertTrue(expressions contains inv3WithBoolInv)      
+    assertTrue(expressions contains inv3WithBoolInv)    
+    assertTrue(expressions contains inv4WithBoolInv)  
+    assertTrue(expressions contains inv4WithInt)   
   }
   
   @Test
@@ -61,20 +62,26 @@ class ReconstructorTest {
     
     val expressions = assertTake(expStream, 20).map(_.snippet)
     
-    val listOfExpressions = List(boolInv, inv1WithInt, inv1WithBoolInv, inv2WithInt,
-      inv3WithInt, inv2WithBoolInv, inv3WithBoolInv)
+    val listOfExpressions = List(inv1boolInv, inv1WithInt, inv2WithBoolInv, inv2WithInt,
+      inv3WithInt, inv3WithBoolInv, inv4WithBoolInv, inv4WithInt)
     
     for (exp <- listOfExpressions)
     	assertTrue(expressions.toSet contains exp)
     	
-    val listOfExpressionsOrder = List(boolInv, inv1WithBoolInv, inv2WithInt,
-      inv2WithBoolInv, inv3WithBoolInv)
+    val listOfExpressionsOrder = List(
+      List(inv1boolInv, inv1WithInt),
+      List(inv2WithBoolInv, inv2WithInt),
+      List(inv3WithInt, inv3WithBoolInv),
+      List(inv4WithBoolInv, inv4WithInt)
+    )
     
-    for (ind <- 0 until listOfExpressionsOrder.size - 1)
-      assertTrue("Expression " + listOfExpressionsOrder(ind) + " (position " + expressions.indexOf(listOfExpressionsOrder(ind)) +
-        ") should occur before expression " + listOfExpressionsOrder(ind+1) + " (position " + expressions.indexOf(listOfExpressionsOrder(ind + 1)) + ")",
-        expressions.indexOf(listOfExpressionsOrder(ind)) < expressions.indexOf(listOfExpressionsOrder(ind+1)))
-      
+    for (ind <- 0 until listOfExpressionsOrder.size - 1) {
+      for( previousEl <- listOfExpressionsOrder(ind); nextEl <- listOfExpressionsOrder(ind + 1) )
+	      assertTrue("Expression " + previousEl + " (position " + expressions.indexOf(previousEl) +
+	        ") should occur before expression " + nextEl + " (position " + expressions.indexOf(nextEl) + ")",
+	        expressions.indexOf(previousEl) < expressions.indexOf(nextEl))
+    }
+  	      
   }
 
 }
diff --git a/src/test/scala/insynth/testutil/CommonDeclarations.scala b/src/test/scala/insynth/testutil/CommonDeclarations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..faca9b3b27c5e1b0764877fe3a46b44f9a725fc5
--- /dev/null
+++ b/src/test/scala/insynth/testutil/CommonDeclarations.scala
@@ -0,0 +1,112 @@
+package insynth.testutil
+
+import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
+
+import org.junit.Assert._
+import org.junit.Test
+import org.junit.Ignore
+
+import insynth.leon.loader.DeclarationFactory._
+import insynth.leon._
+
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ FreshIdentifier }
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+
+object CommonDeclarations {
+  
+  val booleanLiteral = BooleanLiteral(false)
+        
+  val booleanDeclaration = makeDeclaration(
+      ImmediateExpression("false", booleanLiteral),
+      BooleanType
+  )
+  
+  val intLiteral = IntLiteral(0)
+  
+  val intDeclaration = makeDeclaration(
+      ImmediateExpression("0", intLiteral),
+      Int32Type
+  )
+  
+  val unit = UnitLiteral
+    
+  val unitDeclaration = makeDeclaration(
+      ImmediateExpression("unit", unit),
+      UnitType
+  )
+  
+  val functionBoolToIntFunDef = 
+    new FunDef(
+      FreshIdentifier("function1"),
+      Int32Type,
+      List( VarDecl(FreshIdentifier("var"), BooleanType))
+    )
+  
+  val functionBoolToIntType =
+    FunctionType(List(BooleanType), Int32Type)
+      
+  val functionBoolToIntDeclaration = makeDeclaration(
+      NaryReconstructionExpression("function1", { args: List[Expr] => FunctionInvocation(functionBoolToIntFunDef, args) }), 
+      functionBoolToIntType
+    )     
+      
+  val functionFun1ToUnitFunDef = 
+    new FunDef(
+      FreshIdentifier("function2"),
+      UnitType,
+      List( VarDecl(FreshIdentifier("var"), functionBoolToIntType))
+    )  
+  
+  val functionFun1ToUnitType =
+    FunctionType(List(UnitType), functionBoolToIntType)
+      
+  val functionFun1ToUnitDeclaration = makeDeclaration(
+      NaryReconstructionExpression("function2", { args: List[Expr] => FunctionInvocation(functionFun1ToUnitFunDef, args) }), 
+      functionFun1ToUnitType
+    )     
+   
+  val functionIntToIntType =
+    FunctionType(List(Int32Type), Int32Type)
+  
+  val functionIntToIntFunDef= {
+    val varId = FreshIdentifier("var")
+    val varDec = VarDecl(varId, Int32Type)
+    
+    val funDef = new FunDef(
+      FreshIdentifier("functionRec"),
+      Int32Type,
+      List( varDec )
+    )
+    
+    funDef.body = Some(Variable(varId))
+    
+    funDef
+  }
+  
+  val functionIntToIntDeclaration = makeDeclaration(
+    NaryReconstructionExpression("functionRec", { args: List[Expr] => FunctionInvocation(functionIntToIntFunDef, args) }), 
+    functionIntToIntType
+  )
+  
+  val threeParFunctionType =
+    FunctionType(List(Int32Type, Int32Type, BooleanType), Int32Type)
+    
+  val threeParFunctionDef = 
+    new FunDef(
+      FreshIdentifier("function3"),
+      Int32Type,
+      List(
+        VarDecl(FreshIdentifier("var_1"), Int32Type),
+        VarDecl(FreshIdentifier("var_2"), Int32Type),
+        VarDecl(FreshIdentifier("var_3"), BooleanType)
+      )
+    )
+  
+  val threeParFunctionDeclaration = makeDeclaration(
+      NaryReconstructionExpression("function3", { args: List[Expr] => FunctionInvocation(threeParFunctionDef, args) }), 
+      threeParFunctionType
+    )
+  
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/testutil/CommonLambda.scala b/src/test/scala/insynth/testutil/CommonLambda.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e5dc73cb42a49da548bfcb03f0a96c40509bfb61
--- /dev/null
+++ b/src/test/scala/insynth/testutil/CommonLambda.scala
@@ -0,0 +1,186 @@
+package insynth.testutil
+
+import insynth.leon.{ LeonQueryBuilder => QueryBuilder, _ }
+import insynth.reconstruction.stream._
+
+import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
+import leon.purescala.Common.{ FreshIdentifier }
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees.{ Variable => _, _ }
+
+object CommonLambda {
+
+  implicit val leonToDomainType = DomainTypeTransformer(_: TypeTree)
+
+  import CommonDeclarations._
+  import CommonProofTrees._
+      
+  val booleanIdentifier = Identifier(BooleanType, booleanDeclaration)
+  
+  def constructBooleanToIntIntermediateLambda = {
+    val query = new QueryBuilder(Int32Type)
+
+    val functionApplication =
+      Application(
+        functionIntToIntType,
+        List(
+          Identifier(functionBoolToIntType, functionBoolToIntDeclaration),
+          booleanIdentifier))
+
+    val intermediateTree =
+      Application(
+        query.leonType,
+        List(
+          Identifier(query.leonType, query.getQuery.getDeclaration),
+          functionApplication))
+
+    List(intermediateTree)
+  }
+  
+  def constructIntToIntIntermediateFirstLambda(x: Int) = {
+    val query = new QueryBuilder(Int32Type)
+
+    val functionApplication =
+      Application(
+        functionIntToIntType,
+        List(
+          Identifier(functionIntToIntType, functionIntToIntDeclaration),
+          Identifier(Int32Type, intDeclaration)))
+
+    val (_, listOfApplication) =
+      (((Identifier(Int32Type, intDeclaration), Nil): (Node, List[Node])) /: (1 to x)) {
+      	case ((nextArg, list), _) =>
+		      val app =	Application(
+		        functionIntToIntType,
+		        List(Identifier(functionIntToIntType, functionIntToIntDeclaration),
+		          nextArg))
+		          
+          (app, list :+ app)
+    	}
+    
+    for (app <- listOfApplication) yield 
+    	Application(
+        query.leonType,
+        List(
+          Identifier(query.leonType, query.getQuery.getDeclaration),
+          app))    
+  }    
+  
+  def constructIntAndBoolToIntIntermediateLambda(x: Int) = {
+    val query = new QueryBuilder(Int32Type)
+
+    val functionApplicationBoolean =
+      Application(
+        functionBoolToIntType,
+        List(
+          Identifier(functionBoolToIntType, functionBoolToIntDeclaration),
+          booleanIdentifier))
+          
+    val functionApplication =
+      Application(
+        functionIntToIntType,
+        List(
+          Identifier(functionIntToIntType, functionIntToIntDeclaration),
+          Identifier(Int32Type, intDeclaration)))
+
+    val (listOfApplication, _) =
+      (((Nil, List(Identifier(Int32Type, intDeclaration), functionApplicationBoolean)): (List[Node], List[Node])) /: (1 to x)) {
+      	case ((list, args), _) =>
+		      val listAddition =
+		        for (arg <- args) yield
+			        Application(functionIntToIntType,
+		        		List(Identifier(functionIntToIntType, functionIntToIntDeclaration), arg))
+		          
+          (list ++ listAddition, listAddition)
+    	}
+    
+    for (app <- listOfApplication) yield 
+    	Application(
+        query.leonType,
+        List(
+          Identifier(query.leonType, query.getQuery.getDeclaration),
+          app))    
+  }  
+  
+  def constructThreeParFunctionIntermediateLambda(x: Int) = {
+    val query = new QueryBuilder(Int32Type)
+
+    val listOfApplication =
+      ((List(Identifier(Int32Type, intDeclaration), Identifier(Int32Type, intDeclaration)): List[Node]) /: (1 to x)) {
+      	case (list, _) =>
+		      val listAddition =
+		        (for (arg <- list.combinations(2)) yield
+			        Application(
+					      threeParFunctionType,
+					      List(
+					        Identifier(threeParFunctionType, threeParFunctionDeclaration),
+					        arg(0),
+					        arg(1),
+					        booleanIdentifier         
+					      )
+					    )) ++		      	
+		        (for (arg <- list.combinations(2)) yield
+			        Application(
+					      threeParFunctionType,
+					      List(
+					        Identifier(threeParFunctionType, threeParFunctionDeclaration),
+					        arg(1),
+					        arg(0),
+					        booleanIdentifier         
+					      )
+					    ))  ++		      	
+		        (for (arg <- list) yield
+			        Application(
+					      threeParFunctionType,
+					      List(
+					        Identifier(threeParFunctionType, threeParFunctionDeclaration),
+					        arg, arg,
+					        booleanIdentifier         
+					      )
+					    ))				    
+		          
+          (list ++ listAddition).distinct
+    	}
+    
+    for (app <- listOfApplication.distinct) yield 
+    	Application(
+        query.leonType,
+        List(
+          Identifier(query.leonType, query.getQuery.getDeclaration),
+          app))
+  }
+  
+  // TODO do if we need abstraction (high-order functions)
+//  def constructFunctionIntToIntIntermediateLambda = {
+//    val query = new QueryBuilder(FunctionType(List(Int32Type), Int32Type))
+//
+//    val functionApplicationBoolean =
+//      Application(
+//        functionBoolToIntType,
+//        List(
+//          Set(Identifier(functionIntToIntType, functionBoolToIntDeclaration)),
+//          Set(booleanIdentifier)))
+//          
+//    val functionApplication =
+//      Application(
+//        functionIntToIntType,
+//        List(
+//          Set(Identifier(functionIntToIntType, functionIntToIntDeclaration)),
+//          Set(Variable(Int32Type, "freshInt"), functionApplicationBoolean)))
+//
+//    functionApplication.recursiveParams = List(Set(functionApplication))
+//	
+//		val abstraction = Abstraction(functionIntToIntType,
+//	    List(Variable(Int32Type, "var_1")), Set(functionApplicationBoolean, functionApplication))
+//
+//    val intermediateTree =
+//      Application(
+//        query.leonType,
+//        List(
+//          Set(Identifier(query.leonType, query.getQuery.getDeclaration)),
+//          Set(abstraction)))
+//
+//    intermediateTree
+//  }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala b/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
index 2ce2d4246934eee65c4cca31a1ef15e51b5ce7a5..1ab08d1b45f0cea2138f6dd56249a2c7e303381c 100644
--- a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
+++ b/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
@@ -9,12 +9,13 @@ object CommonLeonExpressions {
 
   import CommonDeclarations._
         
-  val boolInv = FunctionInvocation(functionBoolToIntFunDef, List(booleanLiteral))
-  val inv1WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(boolInv))
+  val inv1boolInv = FunctionInvocation(functionBoolToIntFunDef, List(booleanLiteral))
+  val inv2WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(inv1boolInv))
   val inv1WithInt = FunctionInvocation(functionIntToIntFunDef, List(intLiteral))
   val inv2WithInt = FunctionInvocation(functionIntToIntFunDef, List(inv1WithInt))
   val inv3WithInt = FunctionInvocation(functionIntToIntFunDef, List(inv2WithInt))
-  val inv2WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(inv1WithBoolInv))
   val inv3WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(inv2WithBoolInv))
+  val inv4WithBoolInv = FunctionInvocation(functionIntToIntFunDef, List(inv3WithBoolInv))
+  val inv4WithInt = FunctionInvocation(functionIntToIntFunDef, List(inv3WithInt))
 
 }
\ No newline at end of file
diff --git a/src/test/scala/insynth/testutil/CommonProofTrees.scala b/src/test/scala/insynth/testutil/CommonProofTrees.scala
new file mode 100644
index 0000000000000000000000000000000000000000..82f5adac4ccdbca1ffbd40f039cab649429c19a1
--- /dev/null
+++ b/src/test/scala/insynth/testutil/CommonProofTrees.scala
@@ -0,0 +1,218 @@
+package insynth.testutil
+
+import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
+
+import org.junit.Assert._
+import org.junit.Test
+import org.junit.Ignore
+
+import insynth.leon.{ LeonQueryBuilder => QueryBuilder, _ }
+import insynth.structures._
+
+import leon.purescala.TypeTrees._
+import leon.purescala.Trees._
+
+object CommonProofTrees {
+
+  import CommonDeclarations._
+
+  def exampleBoolToInt = {
+    val queryBuilder = new QueryBuilder(Int32Type)
+
+    val query = queryBuilder.getQuery
+
+    val queryDeclaration = query.getDeclaration
+
+    val getBooleanNode =
+      new SimpleNode(
+        List(booleanDeclaration),
+        MutableMap.empty)
+
+    val getIntNode =
+      new SimpleNode(
+        List(functionBoolToIntDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Boolean") ->
+            new ContainerNode(
+              MutableSet(getBooleanNode))))
+
+    val queryNode =
+      new SimpleNode(
+        List(queryDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Int") ->
+            new ContainerNode(
+              MutableSet(getIntNode))))
+
+    (queryNode, query)
+  }
+
+  def exampleIntToInt = {
+    val queryBuilder = new QueryBuilder(Int32Type)
+
+    val query = queryBuilder.getQuery
+
+    val queryDeclaration = query.getDeclaration
+
+    val intNode =
+      new SimpleNode(
+        List(intDeclaration),
+        MutableMap.empty)
+
+    val getIntNode =
+      new SimpleNode(
+        List(functionIntToIntDeclaration),
+        MutableMap())
+
+    getIntNode.getParams +=
+      (
+        Const("Int") ->
+        new ContainerNode(
+          MutableSet(intNode, getIntNode)))
+
+    val queryNode =
+      new SimpleNode(
+        List(queryDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Int") ->
+            new ContainerNode(
+              MutableSet(getIntNode))))
+
+    queryNode
+  }
+  
+  
+  def exampleIntToIntBool = {
+    val queryBuilder = new QueryBuilder(Int32Type)
+
+    val query = queryBuilder.getQuery
+
+    val queryDeclaration = query.getDeclaration
+                    
+    val getBooleanNode =
+      new SimpleNode(
+        List(booleanDeclaration),
+        MutableMap.empty)
+
+    val getIntNodeFromBoolean =
+      new SimpleNode(
+        List(functionBoolToIntDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Boolean") ->
+            new ContainerNode(
+              MutableSet(getBooleanNode))))
+
+    val getIntNodeFromIntToInt =
+      new SimpleNode(
+        List(functionIntToIntDeclaration),
+        MutableMap())
+
+    getIntNodeFromIntToInt.getParams +=
+      (
+        Const("Int") ->
+        new ContainerNode(
+          MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt)))
+
+    val queryNode =
+      new SimpleNode(
+        List(queryDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Int") ->
+            new ContainerNode(
+              MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt))))
+
+    queryNode
+  }
+  
+  
+  def exampleIntToIntBoth = {
+    val queryBuilder = new QueryBuilder(Int32Type)
+
+    val query = queryBuilder.getQuery
+
+    val queryDeclaration = query.getDeclaration
+        
+    val intNode =
+      new SimpleNode(
+        List(intDeclaration),
+        MutableMap.empty)
+                    
+    val getBooleanNode =
+      new SimpleNode(
+        List(booleanDeclaration),
+        MutableMap.empty)
+
+    val getIntNodeFromBoolean =
+      new SimpleNode(
+        List(functionBoolToIntDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Boolean") ->
+            new ContainerNode(
+              MutableSet(getBooleanNode))))
+
+    val getIntNodeFromIntToInt =
+      new SimpleNode(
+        List(functionIntToIntDeclaration),
+        MutableMap())
+
+    getIntNodeFromIntToInt.getParams +=
+      (
+        Const("Int") ->
+        new ContainerNode(
+          MutableSet(intNode, getIntNodeFromBoolean, getIntNodeFromIntToInt)))
+
+    val queryNode =
+      new SimpleNode(
+        List(queryDeclaration),
+        MutableMap( // for each parameter type - how can we resolve it
+          Const("Int") ->
+            new ContainerNode(
+              MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt))))
+
+    queryNode
+  }
+  
+  // TODO do if we need abstraction (high-order functions)
+//  def exampleFunctionIntToInt = {
+//    val queryBuilder = new QueryBuilder(FunctionType(List(Int32Type), Int32Type))
+//
+//    val query = queryBuilder.getQuery
+//
+//    val queryDeclaration = query.getDeclaration
+//                    
+//    val getBooleanNode =
+//      new SimpleNode(
+//        List(booleanDeclaration),
+//        MutableMap.empty)
+//
+//    val getIntNodeFromBoolean =
+//      new SimpleNode(
+//        List(functionBoolToIntDeclaration),
+//        MutableMap( // for each parameter type - how can we resolve it
+//          Const("Boolean") ->
+//            new ContainerNode(
+//              MutableSet(getBooleanNode))))
+//
+//    val getIntNodeFromIntToInt =
+//      new SimpleNode(
+//        List(functionIntToIntDeclaration),
+//        MutableMap())
+//
+//    getIntNodeFromIntToInt.getParams +=
+//      (
+//        Const("Int") ->
+//        new ContainerNode(
+//          MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt)))
+//
+//    val queryNode =
+//      new SimpleNode(
+//        List(queryDeclaration),
+//        MutableMap( // for each parameter type - how can we resolve it
+//          Const("Int") ->
+//            new ContainerNode(
+//              MutableSet(getIntNodeFromBoolean, getIntNodeFromIntToInt))))
+//
+//    queryNode
+//  }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/insynth/testutil/CommonUtils.scala b/src/test/scala/insynth/testutil/CommonUtils.scala
new file mode 100644
index 0000000000000000000000000000000000000000..406452b93a799cb93b33108c113fb6e9649bcfa8
--- /dev/null
+++ b/src/test/scala/insynth/testutil/CommonUtils.scala
@@ -0,0 +1,20 @@
+package insynth.testutil
+
+import org.junit.Assert._
+
+import insynth.reconstruction.Output
+
+object CommonUtils {
+    
+  val maxElToOutput = 20
+      
+  def assertTake(stream: Stream[Output], num: Int) = {
+    val result = stream take num
+    val message = "Part of the resulting stream: " + result.take(maxElToOutput).mkString("\n")
+    
+    for (ind <- 0 until result.size - 1)
+      assertTrue("Weight are not in non-decreasing order.\n" + "At position " + ind + "\n" + message, stream(ind).getWeight <= stream(ind + 1).getWeight)
+    result
+  }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/EnumerationFastTest.scala b/src/test/scala/lesynth/EnumerationFastTest.scala
deleted file mode 100644
index 7eccbb25a1cb2cb3a6107c2c268ee6e5538aadd3..0000000000000000000000000000000000000000
--- a/src/test/scala/lesynth/EnumerationFastTest.scala
+++ /dev/null
@@ -1,182 +0,0 @@
-package lesynth
-
-import org.scalatest.FunSuite
-import org.scalatest.matchers.ShouldMatchers._
-
-import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import java.io.{ BufferedWriter, FileWriter, File }
-import leon.evaluators.CodeGenEvaluator
-import leon.purescala.TreeOps
-import leon.purescala.Common._
-import leon.codegen.CodeGenEvalParams
-import leon.purescala.TypeTrees._
-import leon.evaluators.EvaluationResults._
-
-import insynth._
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
-
-import lesynth.refinement._
-import lesynth.examples._
-import lesynth.evaluation.CodeGenEvaluationStrategy
-import lesynth.ranking.Candidate
-import insynth.reconstruction.Output
-
-import insynth.util._
-import lesynth.util._
-
-class EnumerationFastTest extends FunSuite {
-
-  import Scaffold._
-  import TestConfig._
-  
-  val CANDIDATES_TO_ENUMERATE = 50 :: 100 :: 1000 :: 10000 :: Nil
-  
-  val files = List("InsertionSortInsert.scala", "ListConcat.scala", "MergeSortSort.scala",
-		"RedBlackTreeInsert.scala") map { lesynthTestDir + _ }
-
-  ignore("Candidate enumeration duplicates") {
-        
-    for (candidatesToEnumerate <- CANDIDATES_TO_ENUMERATE; 
-      file <- files;
-    	(sctx, funDef, problem) <- forFile(file)) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-	    val builder = new InitialEnvironmentBuilder(allDeclarations)
-	    
-	    val outputs = inSynth.getExpressions(builder)
-	          
-      val taken = outputs.take(candidatesToEnumerate).map(_.getSnippet).toList
-      val takenDistinct = taken.distinct
-      val takenRepeated = taken.filter(snip => taken.count(_ == snip) > 1)
-      
-      assert(taken.size == takenDistinct.size, "First " + candidatesToEnumerate +
-        " are not distinct." +
-        "Repeated #" + takenRepeated.size
-        	+ ": " + takenRepeated.map(snip => snip.toString +
-      	    " repeats " + taken.count(_ == snip)).mkString("\n")
-      )
-      assert(takenRepeated.isEmpty)
-    }
-  }
-  
-  test("Enumeration in Address example") {
-        
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      for (decl <- newDeclarations)
-        println(decl.getSimpleName)
-	    
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-            
-//	    val solver = inSynth.solver
-//	    solver.getProofTree(builder)
-//	    val solution = solver.getProofTree
-//	    
-//	    import ProofTreeOperations._
-//	    assert(ProofTreeOperations.checkInhabitants(solution,
-//        StringNode("AddressBook", Set(
-//            //StringNode("[Cons=>List]", Set(StringNode("Cons"))),
-//            StringNode("makeAddressBook", Set(StringNode("tail")))
-//          ))
-//        ))
-	    
-	    val outputs = inSynth.getExpressions(builder)
-	    
-      for (output <- outputs.take(20000))
-        printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
-	    
-//	    val proofTree = inSynth.solver.getProofTree(builder)
-//	    val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
-//	    insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
-    }
-    
-  }
-  
-  ignore("Enumeration in Address (mergeAddressBooks) example") {
-        
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-//		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-//		  	get.asInstanceOf[CaseClassDef]
-//	    val listVal = funDef.args.head.toVariable
-//      
-//      val variableRefiner = 
-//  			new VariableRefiner(loader.directSubclassesMap,
-//  					loader.variableDeclarations, loader.classMap)
-//      
-//	    val (refined, newDeclarations) = 
-//	      variableRefiner.checkRefinements(
-//          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-//      assert(refined)
-//      assert(allDeclarations.size + 2 == newDeclarations.size)
-//      
-//      for (decl <- newDeclarations)
-//        println(decl.getSimpleName)
-//	    
-//	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-	    //assert(inSynth.getCurrentBuilder.getAllDeclarations.size > 13, { throw new RuntimeException; "aaa" })
-//	    assert(false)
-	    
-	    val outputs = inSynth.getExpressions//(builder)
-	    
-//	    val proofTree = inSynth.solver.getProofTree(builder)
-//	    val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
-//	    insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
-	          
-      for (output <- outputs.take(20000))
-        printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
-    }
-    
-  }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/EnumerationTest.scala b/src/test/scala/lesynth/EnumerationTest.scala
deleted file mode 100644
index b1a1efd5c238f96220c91c71988a5e0edb652980..0000000000000000000000000000000000000000
--- a/src/test/scala/lesynth/EnumerationTest.scala
+++ /dev/null
@@ -1,230 +0,0 @@
-package lesynth
-
-import org.scalatest.FunSuite
-import org.scalatest.matchers.ShouldMatchers._
-
-import leon._
-import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import java.io.{ BufferedWriter, FileWriter, File }
-import leon.evaluators.CodeGenEvaluator
-import leon.purescala.TreeOps
-import leon.purescala.Common._
-import leon.codegen.CodeGenEvalParams
-import leon.purescala.TypeTrees._
-import leon.evaluators.EvaluationResults._
-
-import insynth._
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
-
-import lesynth.refinement._
-import lesynth.examples._
-import lesynth.evaluation.CodeGenEvaluationStrategy
-import lesynth.ranking.Candidate
-import insynth.reconstruction.Output
-
-import insynth.util._
-import lesynth.util._
-
-class EnumerationTest extends FunSuite {
-
-  import Scaffold._
-  import TestConfig._
-  
-  val CANDIDATES_TO_ENUMERATE = 50 :: 100 :: 1000 :: 10000 :: Nil
-  
-  val files = List("InsertionSortInsert.scala", "ListConcat.scala", "MergeSortSort.scala",
-		"RedBlackTreeInsert.scala") map { lesynthTestDir + _ }
-
-  ignore("Candidate enumeration duplicates") {
-        
-    for (candidatesToEnumerate <- CANDIDATES_TO_ENUMERATE; 
-      file <- files;
-    	(sctx, funDef, problem) <- forFile(file)) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynth(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-	    val builder = new InitialEnvironmentBuilder(allDeclarations)
-	    
-	    val outputs = inSynth.getExpressions(builder)
-	          
-      val taken = outputs.take(candidatesToEnumerate).map(_.getSnippet).toList
-      val takenDistinct = taken.distinct
-      val takenRepeated = taken.filter(snip => taken.count(_ == snip) > 1)
-      
-      assert(taken.size == takenDistinct.size, "First " + candidatesToEnumerate +
-        " are not distinct." +
-        "Repeated #" + takenRepeated.size
-        	+ ": " + takenRepeated.map(snip => snip.toString +
-      	    " repeats " + taken.count(_ == snip)).mkString("\n")
-      )
-      assert(takenRepeated.isEmpty)
-    }
-  }
-  
-  ignore("Enumeration in Address example") {
-        
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynth(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-		  	get.asInstanceOf[CaseClassDef]
-	    val listVal = funDef.args.head.toVariable
-      
-      val variableRefiner = 
-  			new VariableRefiner(loader.directSubclassesMap,
-  					loader.variableDeclarations, loader.classMap)
-      
-	    val (refined, newDeclarations) = 
-	      variableRefiner.checkRefinements(
-          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-      assert(refined)
-      assert(allDeclarations.size + 2 == newDeclarations.size)
-      
-      for (decl <- newDeclarations)
-        println(decl.getSimpleName)
-	    
-	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-            
-	    val solver = inSynth.solver
-	    solver.getProofTree(builder)
-	    val solution = solver.getProofTree
-	    
-	    import ProofTreeOperations._
-	    assert(ProofTreeOperations.checkInhabitants(solution,
-        StringNode("AddressBook", Set(
-            //StringNode("[Cons=>List]", Set(StringNode("Cons"))),
-            StringNode("makeAddressBook", Set(StringNode("tail")))
-          ))
-        ))
-	    
-	    val outputs = inSynth.getExpressions(builder)
-	    
-//	    val proofTree = inSynth.solver.getProofTree(builder)
-//	    val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
-//	    insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
-	          
-//      for (output <- outputs.take(20000))
-//        printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
-    }
-    
-  }
-  
-  ignore("Enumeration in Address (mergeAddressBooks) example") {
-        
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynth(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-//		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-//		  	get.asInstanceOf[CaseClassDef]
-//	    val listVal = funDef.args.head.toVariable
-//      
-//      val variableRefiner = 
-//  			new VariableRefiner(loader.directSubclassesMap,
-//  					loader.variableDeclarations, loader.classMap)
-//      
-//	    val (refined, newDeclarations) = 
-//	      variableRefiner.checkRefinements(
-//          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-//      assert(refined)
-//      assert(allDeclarations.size + 2 == newDeclarations.size)
-//      
-//      for (decl <- newDeclarations)
-//        println(decl.getSimpleName)
-//	    
-//	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-	    //assert(inSynth.getCurrentBuilder.getAllDeclarations.size > 13, { throw new RuntimeException; "aaa" })
-//	    assert(false)
-	    
-	    val outputs = inSynth.getExpressions//(builder)
-	    
-//	    val proofTree = inSynth.solver.getProofTree(builder)
-//	    val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
-//	    insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
-	          
-      for (output <- outputs.take(20000))
-        printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
-    }
-    
-  }
-  
-  test("Enumeration in Address (mergeAddressBooks) example with fast reconstructor") {
-        
-    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
-      val program = sctx.program
-      val arguments = funDef.args.map(_.id)
-
-      expect(1) { problem.xs.size }
-      val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
-
-	    val loader = new LeonLoader(program, hole, problem.as, false)
-	    val inSynth = new InSynthTemp(loader, true)
-	    // save all declarations seen
-	    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
-	    
-//		  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
-//		  	get.asInstanceOf[CaseClassDef]
-//	    val listVal = funDef.args.head.toVariable
-//      
-//      val variableRefiner = 
-//  			new VariableRefiner(loader.directSubclassesMap,
-//  					loader.variableDeclarations, loader.classMap)
-//      
-//	    val (refined, newDeclarations) = 
-//	      variableRefiner.checkRefinements(
-//          CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
-//      assert(refined)
-//      assert(allDeclarations.size + 2 == newDeclarations.size)
-//      
-//      for (decl <- newDeclarations)
-//        println(decl.getSimpleName)
-//	    
-//	    val builder = new InitialEnvironmentBuilder(newDeclarations)
-	    //assert(inSynth.getCurrentBuilder.getAllDeclarations.size > 13, { throw new RuntimeException; "aaa" })
-//	    assert(false)
-	    
-	    val outputs = inSynth.getExpressions//(builder)
-	    
-//	    val proofTree = inSynth.solver.getProofTree(builder)
-//	    val os = new java.io.PrintWriter(new java.io.FileOutputStream("proofTree.xml"))
-//	    insynth.util.format.TreePrinter.printAnswerAsXML(os, proofTree, 6)
-	          
-      for (output <- outputs.take(20000))
-        printf("%20s %5f\n", output.getSnippet.toString, output.getWeight)
-    }
-    
-  }
-
-}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/EvaluationTest.scala b/src/test/scala/lesynth/EvaluationTest.scala
index 8a60f432bc4e7e8e494ef3d1c121938d6d69e854..59b04e930dcb345d9bba56e969b5117d6f9b70e2 100644
--- a/src/test/scala/lesynth/EvaluationTest.scala
+++ b/src/test/scala/lesynth/EvaluationTest.scala
@@ -20,8 +20,9 @@ import lesynth.ranking.Candidate
 import insynth.reconstruction.Output
 import lesynth.examples.Example
 
-import lesynth.util.Scaffold
+import _root_.util.Scaffold
 
+// TODO codegen evaluator params should be used but not yet in master
 class EvaluationTest extends FunSuite {
 
   import Scaffold._
@@ -134,13 +135,12 @@ class EvaluationTest extends FunSuite {
       val program = sctx.program
       val arguments = funDef.args.map(_.id)
 
-      expect(1) { problem.xs.size }
+      expectResult(1) { problem.xs.size }
       val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
 
       val codeGenEval = new CodeGenEvaluator(sctx.context, program)
       def inputExamples =
-        InputExamples.getDataGenInputExamples(codeGenEval, problem,
+        InputExamples.getDataGenInputExamples(sctx.context, program, codeGenEval, problem,
           20, 2000, Some(arguments)).map(Example(_))
 
       import TreeOps._
@@ -154,11 +154,11 @@ class EvaluationTest extends FunSuite {
 
       val body1 =
         searchAndReplace(replaceFun)(
-          program.definedFunctions.find(_.id.name == "testFun1").get.getBody)
+          program.definedFunctions.find(_.id.name == "testFun1").get.body.get)
 
       val body2 =
         searchAndReplace(replaceFun)(
-          program.definedFunctions.find(_.id.name == "testFun2").get.getBody)
+          program.definedFunctions.find(_.id.name == "testFun2").get.body.get)
 
       val evaluationStrategy = new CodeGenEvaluationStrategy(program, funDef, sctx.context, 500)
 
@@ -191,13 +191,12 @@ class EvaluationTest extends FunSuite {
       val program = sctx.program
       val arguments = funDef.args.map(_.id)
 
-      expect(1) { problem.xs.size }
+      expectResult(1) { problem.xs.size }
       val resultVariable = problem.xs.head
-      val hole = Hole(resultVariable.getType)
 
       val codeGenEval = new CodeGenEvaluator(sctx.context, program)
       def inputExamples =
-        InputExamples.getDataGenInputExamples(codeGenEval, problem,
+        InputExamples.getDataGenInputExamples(sctx.context, program, codeGenEval, problem,
           20, 2000, Some(arguments)).map(Example(_))
 
       import TreeOps._
@@ -209,10 +208,10 @@ class EvaluationTest extends FunSuite {
 
       val body1 =
         searchAndReplace(replaceFun)(
-          program.definedFunctions.find(_.id.name == "testFun1").get.getBody)
+          program.definedFunctions.find(_.id.name == "testFun1").get.body.get)
       val body2 =
         searchAndReplace(replaceFun)(
-          program.definedFunctions.find(_.id.name == "testFun2").get.getBody)
+          program.definedFunctions.find(_.id.name == "testFun2").get.body.get)
 
       // evaluate expressions with let
       {
@@ -238,11 +237,12 @@ class EvaluationTest extends FunSuite {
           val resFresh = FreshIdentifier("result") //.setType(expr.getType)
           resFresh.setType(newBody.getType)
 
+          val (id, post) = newFun.postcondition.get
           // body can contain (self-)recursive calls
           (
             Let(resFresh, newBody,
-              replace(Map(ResultVariable() -> Variable(resFresh)),
-                matchToIfThenElse(newFun.getPostcondition))),
+              replace(Map(Variable(id) -> Variable(resFresh)),
+                matchToIfThenElse(post))),
               newFun)
         }
 
@@ -252,7 +252,8 @@ class EvaluationTest extends FunSuite {
         val params = CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true)
 
         val evaluator = new CodeGenEvaluator(sctx.context,
-          program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2))), params)
+          program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2)))
+          /*, params*/)
 
         val eval1 = (for (ind <- 0 until inputExamples.size) yield {
           val res = evaluator.eval(candidates(0), inputExamples(ind).map)
@@ -305,7 +306,8 @@ class EvaluationTest extends FunSuite {
         val params = CodeGenEvalParams(maxFunctionInvocations = 500, checkContracts = true)
 
         val evaluator = new CodeGenEvaluator(sctx.context,
-          program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2))), params)
+          program.copy(mainObject = program.mainObject.copy(defs = program.mainObject.defs ++ pairs.map(_._2)))
+          /*, params*/)
 
         val eval1 = (for (ind <- 0 until inputExamples.size) yield {
           val res = evaluator.eval(candidates(0), inputExamples(ind).map)
diff --git a/src/test/scala/lesynth/FilterTest.scala b/src/test/scala/lesynth/FilterTest.scala
index e9b6aab1789b4df5b0d7647cb890c0bd47d0aeab..a308510fadd0c2fb9da17b0920b77d6c6655be25 100644
--- a/src/test/scala/lesynth/FilterTest.scala
+++ b/src/test/scala/lesynth/FilterTest.scala
@@ -4,8 +4,9 @@ import scala.util.Random
 
 import org.junit.Assert._
 import org.junit.{ Test, Ignore, Before }
+import org.scalatest.junit.JUnitSuite
 
-import insynth.leon.loader.{ LeonLoader, HoleExtractor }
+import insynth.leon.loader.LeonLoader
 import insynth.leon._
 
 import _root_.leon.purescala.Trees._
@@ -15,20 +16,20 @@ import _root_.leon.purescala.Definitions._
 
 import lesynth.refinement._
 
-import util._
+import _root_.util._
 
-class FilterTest {
+class FilterTest extends JUnitSuite {
 
-  import TestConfig._
   import TreeOps._
   import Scaffold._
   
+	val lesynthTestDir = "testcases/condabd/test/lesynth/"
+
   val rnd = new Random(System.currentTimeMillis())
   
   var filter: Filter = _
   
   var prog: Program = _
-  var hole: Hole = _
   var funDef: FunDef = _
   var variableRefiner: VariableRefiner = _
   
@@ -40,19 +41,18 @@ class FilterTest {
   @Before
   def extract = {
     
-    val problems = forFile(lesynthTestDir + "refinement/ListConcat.scala")
+    val problems = forFile(lesynthTestDir + "/ListConcat.scala")
 		assertEquals(1, problems.size)		
     
 		val (sctx, funDef, problem) = problems.head		
 		
 		prog = sctx.program
-    hole = Hole(funDef.getBody.getType)           
     this.funDef = funDef
 	
-    val loader = new LeonLoader(prog, hole, problem.as)
+    val loader = new LeonLoader(prog, problem.as, true)
     
     variableRefiner = new VariableRefiner(loader.directSubclassesMap, loader.variableDeclarations,
-  		loader.classMap)
+  		loader.classMap, sctx.reporter)
     
     tail = 
       loader.extractFields.find { 
diff --git a/src/test/scala/lesynth/VariableRefinerTest.scala b/src/test/scala/lesynth/VariableRefinerTest.scala
index 49f30a53e93f0f0b9b207ea4abb9155a6171c1de..dcaae9ee1a1a3ce262e570683069e8c39ff3633f 100644
--- a/src/test/scala/lesynth/VariableRefinerTest.scala
+++ b/src/test/scala/lesynth/VariableRefinerTest.scala
@@ -14,6 +14,8 @@ import insynth.leon._
 
 import lesynth.refinement._
 
+import _root_.util.Scaffold._
+
 class VariableRefinerTest extends FunSpec with GivenWhenThen {    
   
   val listClassId = FreshIdentifier("List")
@@ -50,25 +52,25 @@ class VariableRefinerTest extends FunSpec with GivenWhenThen {
     
     it("should refine if variable is not Nil") {
       
-      given("a VariableRefiner")
+      Given("a VariableRefiner")
       val variableRefiner = new VariableRefiner(
-        directSubclassMap, Seq(listLeonDeclaration), classMap
+        directSubclassMap, Seq(listLeonDeclaration), classMap, reporter
       )
       
-      then("it should return appropriate id and class def")
-      expect(Some((listVal.id, nilAbstractClassDef))) {
+      Then("it should return appropriate id And class def")
+      expectResult(Some((listVal.id, nilAbstractClassDef))) {
       	variableRefiner.getIdAndClassDef(CaseClassInstanceOf(nilAbstractClassDef, listVal))
       }
-      and("return None for some unknown expression")
-      expect(None) {
+      And("return None for some unknown expression")
+      expectResult(None) {
       	variableRefiner.getIdAndClassDef(listVal)
       }
       
-      then("declarations should be updated accordingly")
+      Then("declarations should be updated accordingly")
       val allDeclarations = List(listLeonDeclaration)
-	    expect((true,
+	    expectResult((true,
         LeonDeclaration(
-					ImmediateExpression( "Field(" + consAbstractClassDef + "." + headId + ")",
+					ImmediateExpression( listVal + "." + headId,
             CaseClassSelector(consAbstractClassDef, listVal, headId) ), 
 					  TypeTransformer(Int32Type), Int32Type
 				) :: 
@@ -77,12 +79,13 @@ class VariableRefinerTest extends FunSpec with GivenWhenThen {
 				) :: Nil
   		)) {
         variableRefiner.checkRefinements(CaseClassInstanceOf(nilAbstractClassDef, listVal),
-        BooleanLiteral(true),
-        allDeclarations)
+	        BooleanLiteral(true),
+	        allDeclarations
+        )
       } 
 	    
-      and("after 2nd consequtive call, nothing should happen")   
-	    expect((false, allDeclarations)) {
+      And("after 2nd consequtive call, nothing should happen")   
+	    expectResult((false, allDeclarations)) {
         variableRefiner.checkRefinements(CaseClassInstanceOf(nilAbstractClassDef, listVal),
         BooleanLiteral(true),
         allDeclarations)
diff --git a/src/test/scala/lesynth/VariableSolverRefinerTest.scala b/src/test/scala/lesynth/VariableSolverRefinerTest.scala
index ba09ed5002ee1667982b98711e1fee275e83a4bf..52175cd08dc67ca8b63c21fb4dcf2bf1b76bdeae 100644
--- a/src/test/scala/lesynth/VariableSolverRefinerTest.scala
+++ b/src/test/scala/lesynth/VariableSolverRefinerTest.scala
@@ -16,23 +16,24 @@ import insynth.leon.loader._
 
 import lesynth.refinement._
 
-import lesynth.util._
+import _root_.util._
+
+class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
 
-class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {    
-  
   import Scaffold._
-  import TestConfig._
+
+	val lesynthTestDir = "testcases/condabd/test/lesynth/"  
       
   describe("A variable solver refiner with list ADT") {
     
     it("should refine if condition is isEmpty()") {
       
-      for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "refinement/ListConcatWithEmpty.scala")) {
+      for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
         val program = sctx.program
-        val solver = sctx.solver
+        val solver = sctx.solverFactory
+        val reporter = sctx.reporter
         
-		    val hole = Hole(funDef.getBody.getType)
-		    val loader = new LeonLoader(program, hole, problem.as, false)
+		    val loader = new LeonLoader(program, problem.as, false)
         val allDeclarations = loader.load
 //		    val inSynth = new InSynth(loader, true)
 //		    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
@@ -60,10 +61,10 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
 			    TypeTransformer(listAbstractClass), listAbstractClass
 			  )
         
-	      given("a VariableSolverRefiner")
+	      Given("a VariableSolverRefiner")
 	      val declarations = List(listLeonDeclaration)
 	      val variableRefiner = new VariableSolverRefiner(
-	        directSubclassMap, declarations, classMap, solver
+	        directSubclassMap, declarations, classMap, solver, reporter
 	      )
 		    
 	      val res = variableRefiner.checkRefinements(
@@ -72,13 +73,13 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
         		declarations
       		)
       		
-	      then("declarations should be updated accordingly")
-		    expect((true, declarations.size)) {
+	      Then("declarations should be updated accordingly")
+		    expectResult((true, declarations.size)) {
       		(res._1, res._2.size)
 	      }
 		    
-	      and("after 2nd consequtive call, nothing should happen")   
-		    expect((false, res._2)) {
+	      And("after 2nd consequtive call, nothing should happen")   
+		    expectResult((false, res._2)) {
 	        val res2 = variableRefiner.checkRefinements(
         		isEmpty(listVal),
         		isEmpty(listVal),
@@ -86,17 +87,19 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
       		)
       		(res2._1, res2._2)
 	      }
+
+        solver.free()
       }
     }
     
     it("should refine list to Cons if condition is hasContent()") {
       
-      for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "refinement/ListConcatWithEmpty.scala")) {
+      for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
         val program = sctx.program
-        val solver = sctx.solver
+        val solver = sctx.solverFactory
+        val reporter = sctx.reporter
         
-		    val hole = Hole(funDef.getBody.getType)
-		    val loader = new LeonLoader(program, hole, problem.as, false)
+		    val loader = new LeonLoader(program, problem.as, false)
         val allDeclarations = loader.load
 //		    val inSynth = new InSynth(loader, true)
 //		    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
@@ -116,10 +119,10 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
 			    TypeTransformer(listAbstractClass), listAbstractClass
 			  )
         
-	      given("a VariableSolverRefiner")
+	      Given("a VariableSolverRefiner")
 	      val declarations = List(listLeonDeclaration)
 	      val variableRefiner = new VariableSolverRefiner(
-	        directSubclassMap, declarations, classMap, solver
+	        directSubclassMap, declarations, classMap, solver, reporter
 	      )
 		    
 	      val res = variableRefiner.checkRefinements(
@@ -128,13 +131,13 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
         		declarations
       		)
       		
-	      then("declarations should be updated accordingly")
-		    expect((true, declarations.size + 2)) {
+	      Then("declarations should be updated accordingly")
+		    expectResult((true, declarations.size + 2)) {
       		(res._1, res._2.size)
 	      }
 		    
-	      and("after 2nd consequtive call, nothing should happen")   
-		    expect((false, res._2)) {
+	      And("after 2nd consequtive call, nothing should happen")   
+		    expectResult((false, res._2)) {
 	        val res2 = variableRefiner.checkRefinements(
         		hasContent(listVal),
         		hasContent(listVal),
@@ -142,17 +145,18 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
       		)
       		(res2._1, res2._2)
 	      }
+        solver.free()
       }
     }
     
     it("should not refine if condition is isEmptyBad()") {
       
-      for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "refinement/ListConcatWithEmpty.scala")) {
+      for ( (sctx, funDef, problem) <- forFile(lesynthTestDir + "/ListConcatWithEmpty.scala")) {
         val program = sctx.program
-        val solver = sctx.solver
+        val solver = sctx.solverFactory
+        val reporter = sctx.reporter
         
-		    val hole = Hole(funDef.getBody.getType)
-		    val loader = new LeonLoader(program, hole, problem.as, false)
+		    val loader = new LeonLoader(program, problem.as, false)
         val allDeclarations = loader.load
 //		    val inSynth = new InSynth(loader, true)
 //		    val allDeclarations = inSynth.getCurrentBuilder.getAllDeclarations
@@ -180,10 +184,10 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
 			    TypeTransformer(listAbstractClass), listAbstractClass
 			  )
         
-	      given("a VariableSolverRefiner")
+	      Given("a VariableSolverRefiner")
 	      val declarations = List(listLeonDeclaration)
 	      val variableRefiner = new VariableSolverRefiner(
-	        directSubclassMap, declarations, classMap, solver
+	        directSubclassMap, declarations, classMap, solver, reporter
 	      )
 		    
 	      val res = variableRefiner.checkRefinements(
@@ -192,8 +196,8 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
         		declarations
       		)
 		    
-	      then("declarations should not be updated")   
-		    expect((false, res._2)) {
+	      Then("declarations should not be updated")   
+		    expectResult((false, res._2)) {
 	        val res2 = variableRefiner.checkRefinements(
         		isEmptyBad(listVal),
         		isEmptyBad(listVal),
@@ -201,6 +205,8 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
       		)
       		(res2._1, res2._2)
 	      }
+
+          solver.free()
       }
     }
     
@@ -230,4 +236,4 @@ class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
 	  (directSubclassMap, AbstractClassType(listAbstractClassDef), classMap)
   }
   
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/lesynth/VerifierTest.scala b/src/test/scala/lesynth/VerifierTest.scala
index 3eb0c5a604e61f2fcb11548dc3e48124986a64a6..7a41d0e76d982b1363a89b3bbdfb6a6a5a913211 100644
--- a/src/test/scala/lesynth/VerifierTest.scala
+++ b/src/test/scala/lesynth/VerifierTest.scala
@@ -10,81 +10,145 @@ import insynth.leon.loader.LeonLoader
 import _root_.leon.purescala._
 import _root_.leon.evaluators._
 import _root_.leon.solvers._
+import _root_.leon.purescala.Trees._
+import leon.purescala.Common._
+import leon.purescala.Definitions._
+import leon.synthesis.Problem
 
-import util._
+import _root_.util._
 
 class VerifierTest extends FunSpec {
 
   import Utils._
   import Scaffold._
-  import TestConfig._
+
+	val lesynthTestDir = "testcases/condabd/test/lesynth"
+	  
+  def getPostconditionFunction(problem: Problem) = {
+    (list: Iterable[Identifier]) => {
+      (problem.phi /: list) {
+        case ((res, newId)) =>
+        	(res /: problem.as.find(_.name == newId.name)) {
+        	  case ((res, oldId)) =>
+        	    TreeOps.replace(Map(Variable(oldId) -> Variable(newId)), res)
+        	}
+      }
+    }
+  }
 	
 	describe("Concrete verifier: ") {    
-    val testCaseFileName = lesynthTestDir + "/verifier/ListConcat.scala"
+    val testCaseFileName = lesynthTestDir + "/ListConcatVerifierTest.scala"
     
     val problems = forFile(testCaseFileName)
     assert(problems.size == 1)
       
   	for ((sctx, funDef, problem) <- problems) {
   	  
-  	  val timeoutSolver = new TimeoutSolver(sctx.solver, 2000L)
+  	  val timeoutSolver = sctx.solverFactory.withTimeout(2000L)
+  	  
+		  val getNewPostcondition = getPostconditionFunction(problem)
   	
   	  describe("A Verifier") {
   	    it("should verify first correct concat body") {		  	  
-		  	  funDef.body = getFunDefByName(sctx.program, "goodConcat1").body
+  	      val newFunDef = getFunDefByName(sctx.program, "goodConcat1")
+		  	  funDef.body = newFunDef.body
+
+		  	  expectResult(1) { problem.xs.size }
+		  	  funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.args.map(_.id))))
+		  	  funDef.precondition = Some(BooleanLiteral(true)) 
 		  	  
-		  	  val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+		  	  val verifier = new Verifier(timeoutSolver, problem)
 		  	  
-		  	  verifier.analyzeFunction(funDef)._1
+		  	  assert( verifier.analyzeFunction(funDef)._1 )
   	    }  	    
   	    
   	    it("should verify 2nd correct concat body") {		  	  
-		  	  funDef.body = getFunDefByName(sctx.program, "goodConcat2").body
+  	      val newFunDef = getFunDefByName(sctx.program, "goodConcat2")
+		  	  funDef.body = newFunDef.body
+
+		  	  expectResult(1) { problem.xs.size }
+		  	  funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.args.map(_.id))))
+		  	  funDef.precondition = Some(BooleanLiteral(true)) 
 		  	  
-		  	  val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+		  	  val verifier = new Verifier(timeoutSolver, problem)
 		  	  
-		  	  verifier.analyzeFunction(funDef)._1
+		  	  assert( verifier.analyzeFunction(funDef)._1 )
   	    }  	    
   	    
   	    it("should not verify an incorrect concat body") {
-		  	  funDef.body = getFunDefByName(sctx.program, "badConcat1").body
+		  	  val newFunDef = getFunDefByName(sctx.program, "badConcat1")
+		  	  funDef.body = newFunDef.body
+
+		  	  expectResult(1) { problem.xs.size }
+		  	  funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.args.map(_.id))))
+		  	  funDef.precondition = Some(BooleanLiteral(true)) 
 		  	  
-		  	  val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+		  	  val verifier = new Verifier(timeoutSolver, problem)
 		  	  
-		  	  ! verifier.analyzeFunction(funDef)._1
+		  	  assert( ! verifier.analyzeFunction(funDef)._1 )
   	    }
   	  }
-  	}				
+  	  
+  	  timeoutSolver.free
+  	}
 	}
+
+  def getPreconditionFunction(problem: Problem) = {
+    (list: Iterable[Identifier]) => {
+      (problem.pc /: list) {
+        case ((res, newId)) =>
+        	(res /: problem.as.find(_.name == newId.name)) {
+        	  case ((res, oldId)) =>
+        	    TreeOps.replace(Map(Variable(oldId) -> Variable(newId)), res)
+        	}
+      }
+    }
+  }
   
 	describe("Relaxed verifier: ") {    
-    val testCaseFileName = lesynthTestDir + "/verifier/BinarySearchTree.scala"
+    val testCaseFileName = lesynthTestDir + "/BinarySearchTree.scala"
     
     val problems = forFile(testCaseFileName)
     assert(problems.size == 1)
       
   	for ((sctx, funDef, problem) <- problems) {
   	  
-  	  val timeoutSolver = new TimeoutSolver(sctx.solver, 1000L)
+  	  val timeoutSolver = sctx.solverFactory.withTimeout(1000L)
+  	  
+		  val getNewPostcondition = getPostconditionFunction(problem)
+		  val getNewPrecondition = getPreconditionFunction(problem)
   	
   	  describe("A RelaxedVerifier on BST") {
   	    it("should verify a correct member body") {		
-		  	  funDef.body = getFunDefByName(sctx.program, "goodMember").body  	  
+		  	  val newFunDef = getFunDefByName(sctx.program, "goodMember")
+		  	  funDef.body = newFunDef.body
+
+		  	  expectResult(1) { problem.xs.size }
+		  	  funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.args.map(_.id))))
+		  	  funDef.precondition = Some(getNewPrecondition(newFunDef.args.map(_.id)))
 		  	  
-		  	  val verifier = new RelaxedVerifier(timeoutSolver.getNewSolver, problem)
+		  	  val verifier = new RelaxedVerifier(timeoutSolver, problem)
 		  	  
-		  	  verifier.analyzeFunction(funDef)._1
+		  	  assert( verifier.analyzeFunction(funDef)._1 )
   	    }  	    
   	      	    
   	    it("should not verify an incorrect member body") {
-		  	  funDef.body = getFunDefByName(sctx.program, "badMember").body
+		  	  val newFunDef = getFunDefByName(sctx.program, "badMember")
+		  	  funDef.body = newFunDef.body
+
+		  	  expectResult(1) { problem.xs.size }
+		  	  funDef.postcondition = Some((problem.xs.head, getNewPostcondition(newFunDef.args.map(_.id))))
+		  	  funDef.precondition = Some(getNewPrecondition(newFunDef.args.map(_.id)))
 		  	  
-		  	  val verifier = new Verifier(timeoutSolver.getNewSolver, problem)
+		  	  val verifier = new Verifier(timeoutSolver, problem)
 		  	  
-		  	  verifier.analyzeFunction(funDef)._1
+		  	  assert( verifier.analyzeFunction(funDef)._1 )
   	    }
   	  }
-  	}				
+  	  
+  	  timeoutSolver.free
+  	}
+    
 	}
   
 }
diff --git a/src/test/scala/lesynth/enumeration/EnumeratorTest.scala b/src/test/scala/lesynth/enumeration/EnumeratorTest.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6e54425f87f27e5f745e2527d084c47fcb56f902
--- /dev/null
+++ b/src/test/scala/lesynth/enumeration/EnumeratorTest.scala
@@ -0,0 +1,419 @@
+package lesynth
+
+import insynth.InSynth
+import insynth.leon._
+import insynth.leon.loader._
+import insynth.engine._
+
+import insynth.reconstruction._
+import insynth.reconstruction.{ stream => lambda }
+import insynth.reconstruction.stream.{ OrderedStreamFactory }
+import insynth.reconstruction.codegen._
+import insynth.reconstruction.Output
+
+import _root_.leon._
+import _root_.leon.purescala._
+import _root_.leon.purescala.Definitions._
+import _root_.leon.purescala.Common._
+import _root_.leon.purescala.TypeTrees._
+import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
+
+import lesynth.refinement._
+//import lesynth.examples._
+//import lesynth.evaluation.CodeGenEvaluationStrategy
+//import lesynth.ranking.Candidate
+
+import org.junit.{ Test, Ignore }
+import org.junit.Assert._
+import org.scalatest.junit.JUnitSuite
+
+import insynth.util.format._
+import insynth.util._
+
+import _root_.util._
+
+import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
+
+// this suggests we should refactor an enumerator class
+class EnumeratorTest extends JUnitSuite {
+
+  import CommonDeclarations._
+  import CommonProofTrees._
+  import CommonLambda._
+  import DeclarationFactory._
+  
+  import Scaffold._
+  
+	import ProofTreeOperations.StringNode
+
+	val lesynthTestDir = "testcases/condabd/test/lesynth/" 
+    
+  val transformer = Streamer.apply _
+  val codegen = (new CodeGenerator).apply _
+  
+  def assertWeight(pair: Output) =
+    assertEquals("Node " + pair.getSnippet + " does not have size " + pair.getWeight,
+      TreeOps.formulaSize(pair.getSnippet).toFloat, pair.getWeight, 0f)
+    
+  def assertTake(insynth: InSynth, num: Int) = {
+    val result = insynth.getExpressions take num
+
+  // TODO this should be applied
+//    def message(pos: Int) = "Part of the resulting stream: " + result.slice(pos - 10, pos + 10).mkString("\n")
+//    
+//    for (ind <- 0 until result.size)
+//      assertWeight(result(ind))
+//    for (ind <- 0 until result.size - 1)
+//      assertTrue("Weights are not in non-decreasing order.\n" + "At position " + ind + "\n" + message(ind),
+//        result(ind).getWeight <= result(ind + 1).getWeight)
+
+    result.map(_.getSnippet)
+  }
+
+  def assertNoDuplicity(extractorResults: Stream[(lambda.Node, Float)]) = {    
+    // note that duplicates may exist in generated code (e.g. because coercions), but should not before that
+    val duplicityMap = (Map[lambda.Node, Set[(lambda.Node, Float)]]() /: extractorResults) {
+      (resMap, pair) =>
+        val snippet = pair._1
+        resMap + (snippet -> (resMap.getOrElse(snippet, Set.empty) + pair))
+    }
+          
+    lazy val duplicityMessage = 
+      for ( (key, value) <- duplicityMap.filter(_._2.size > 1).take(1)) yield
+        ("Key: " + key) + ("\nValues: " + value.mkString("\n"))        
+      
+    assertTrue(
+      "There are some duplications in generated code:\n" + duplicityMessage,
+      duplicityMap.filter(_._2.size > 1).isEmpty
+    )    
+  }
+  
+  // note, refines first argument
+  def refineListVariable(program: Program, funDef: FunDef,
+    loader: LeonLoader, allDeclarations: List[LeonDeclaration], reporter: Reporter) = {	    
+	  val nilAbstractClassDef = program.definedClasses.find(_.id.name == "Nil").
+	  	get.asInstanceOf[CaseClassDef]
+    val listVal = funDef.args.head.toVariable
+    
+    val variableRefiner = 
+			new VariableRefiner(loader.directSubclassesMap,
+					loader.variableDeclarations, loader.classMap, reporter)
+    
+    val (refined, newDeclarations) = 
+      variableRefiner.checkRefinements(
+        CaseClassInstanceOf(nilAbstractClassDef, listVal), BooleanLiteral(true), allDeclarations)
+    assertTrue(refined)
+    assert(allDeclarations.size + 2 == newDeclarations.size)
+    
+    val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+      newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+    assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "tail"))
+    assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "a"))    
+
+    newDeclarations
+  }
+ 
+  @Test
+  def testAddressesWithRefinementProofTree {  
+  	
+    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader, resultVariable.getType, true)
+	    val allDeclarations = inSynth.getAllDeclarations
+      
+	    val newDeclarations = refineListVariable(program, funDef, loader, allDeclarations, sctx.reporter)
+
+	    val builder = new InitialEnvironmentBuilder(newDeclarations)
+	    val solver = inSynth.solver	    
+	    val solution = solver.getProofTree(builder)
+	          
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("AddressBook", Set(
+            StringNode("[Cons=>List]", Set(StringNode("Cons")))
+            ,
+            StringNode("pers", Set(StringNode("makeAddressBook")))
+          ))
+      ))
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("addToPers", Set(
+          StringNode("makeAddressBook", Set(
+        		StringNode("l.tail", Set())
+          ))
+          , 
+          StringNode("a", Set( ))
+        ))
+      ))
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("addToBusiness", Set(
+          StringNode("makeAddressBook", Set(
+        		StringNode("l.tail", Set())
+          ))
+          , 
+          StringNode("a", Set( ))
+        ))
+      ))
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("addToBusiness", Set(
+          StringNode("makeAddressBook", Set(
+        		StringNode("l.tail", Set())
+          ))
+          , 
+          StringNode("l.a", Set( ))
+        ))
+      ))
+    }
+  }
+      
+  @Test
+  def testAddressesWithRefinementSnippets {  
+  	
+    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+      val reporter = sctx.reporter
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val newDeclarations = refineListVariable(program, funDef, loader, loader.load, reporter)	    
+	    val inSynth = new InSynth(newDeclarations, resultVariable.getType, true)
+
+      val extractedSnipptes = assertTake(inSynth, 1000)
+
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    "AddressBook(Nil, l)",
+  	    "makeAddressBook(l)",
+  	    "addToPers(AddressBook(l, l), l.a)",
+  	    "addToBusiness(makeAddressBook(l), l.a)"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+    }
+  } 
+  
+  @Test
+  def testAddressesMergeWithRefinementSnippets {  
+  	
+    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "AddressesMergeAddressBooks.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+      val reporter = sctx.reporter
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader.load, resultVariable.getType, true)
+
+      val extractedSnipptes = assertTake(inSynth, 15000)
+
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    "AddressBook(ab1.pers, ab2.business)",
+  	    "makeAddressBook(ab1.pers)",
+  	    "AddressBook(merge(ab1.business, ab2.business), merge(ab2.pers, ab1.pers))"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+    }
+  } 
+  
+  @Test
+  def testListConcatWithRefinementSnippets {  
+  	
+    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "ListConcat.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+      val reporter = sctx.reporter
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val newDeclarations = refineListVariable(program, funDef, loader, loader.load, reporter)	
+            
+      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.tail"))
+      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l1.head"))    
+
+	    val inSynth = new InSynth(newDeclarations, resultVariable.getType, true)
+
+      val extractedSnipptes = assertTake(inSynth, 1000)
+
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    "concat(Nil(), l1)",
+  	    "Cons(l1.head, Nil())",
+  	    "Cons(l1.head, concat(l1.tail, l2))"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+      
+    }
+  } 
+  
+  @Test
+  def testAddressesWithRefinementBooleanSnippets {  
+  	
+    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+      val reporter = sctx.reporter
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val newDeclarations = refineListVariable(program, funDef, loader, loader.load, reporter)	
+            
+      val declsMessage = "newDeclarations do not contain needed declaration\nnewDeclarations: " +
+        newDeclarations.map(decl => decl.getSimpleName + ":" + decl.getType).mkString("\n")
+      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.a"))
+      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName contains "l.tail")) 
+      assertTrue(declsMessage, newDeclarations.exists(_.getSimpleName == "l"))     
+
+	    val inSynth = new InSynth(newDeclarations, BooleanType, true)
+
+      val extractedSnipptes = assertTake(inSynth, 5000)
+
+      val message = "Extracted: " + extractedSnipptes.size + "\n" +
+        (for (output <- extractedSnipptes)
+        	yield "%20s" format output).mkString("\n")
+        	
+    	val expectedSnipptes = List(
+  	    // FIXME!
+  	    // this one is harder to get since it has coercion for l
+//  	    "allBusiness(AddressBook(Nil, l).pers)",
+//  	    "allBusiness(AddressBook(Nil, l.tail).pers)",
+  	    "allBusiness(makeAddressBook(l).business)",
+  	    "allBusiness(l.tail)",
+  	    "allPrivate(addToBusiness(makeAddressBook(l), l.a).pers)"
+	    )
+      
+	    for (snippet <- expectedSnipptes)
+	    	assertTrue(snippet + " not found in extracted. results:\n" + message,
+    			extractedSnipptes.exists(_.toString == snippet.toString)
+  			)
+    }
+  } 
+ 
+  @Test
+  def testAddressesWithRefinementBooleanProofTree {  
+  	
+    for ((sctx, funDef, problem) <- forFile(lesynthTestDir + "Addresses.scala")) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader, BooleanType, true)
+	    val allDeclarations = inSynth.getAllDeclarations
+      
+	    val newDeclarations = refineListVariable(program, funDef, loader, allDeclarations, sctx.reporter)
+
+	    val builder = new InitialEnvironmentBuilder(newDeclarations)
+	    val solver = inSynth.solver	    
+	    val solution = solver.getProofTree(builder)
+	          
+	    assertTrue(
+		    ProofTreeOperations.breadthFirstSearchPrint(solution.getNodes.head),
+        ProofTreeOperations.checkInhabitants(solution,
+        StringNode("allBusiness", Set(
+	        StringNode("pers", Set(
+		        StringNode("AddressBook", Set(
+	            StringNode("[Nil=>List]", Set(StringNode("Nil", Set())))
+	            ,
+	            StringNode("[Cons=>List]", Set(StringNode("l", Set())))
+	            ,
+	            StringNode("l.tail", Set())
+	          ))
+          ))
+        ))
+      ))
+	    
+    }
+  }
+  
+  val CANDIDATES_TO_ENUMERATE = 50 :: 100 :: 1000 :: 10000 :: Nil
+  
+  val files = List("InsertionSortInsert.scala", "ListConcat.scala", "MergeSortSort.scala",
+		"RedBlackTreeInsert.scala") map { lesynthTestDir + _ }
+
+  @Ignore
+  @Test
+  def candidateEnumerationDuplicatesTest {
+        
+    for (candidatesToEnumerate <- CANDIDATES_TO_ENUMERATE; 
+      file <- files;
+    	(sctx, funDef, problem) <- forFile(file)) {
+      val program = sctx.program
+      val arguments = funDef.args.map(_.id)
+      val reporter = sctx.reporter
+
+      assertEquals(1, problem.xs.size)
+      val resultVariable = problem.xs.head
+      val varsInScope = problem.as
+
+	    val loader = new LeonLoader(program, varsInScope, false)
+	    val inSynth = new InSynth(loader.load, resultVariable.getType, true)
+	    
+	    val outputs = inSynth.getExpressions
+	          
+      val taken = outputs.take(candidatesToEnumerate).map(_.getSnippet).toList
+      val takenDistinct = taken.distinct
+      val takenRepeated = taken.filter(snip => taken.count(_ == snip) > 1)
+      
+      assert(taken.size == takenDistinct.size, "First " + candidatesToEnumerate +
+        " are not distinct." +
+        "Repeated #" + takenRepeated.size
+        	+ ": " + takenRepeated.map(snip => snip.toString +
+      	    " repeats " + taken.count(_ == snip)).mkString("\n")
+      )
+      assert(takenRepeated.isEmpty)
+    }
+  }
+
+}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/util/TestConfig.scala b/src/test/scala/lesynth/util/TestConfig.scala
deleted file mode 100644
index 49eeeb5f3270b1461671183bcbf8d2bbe7b4b2af..0000000000000000000000000000000000000000
--- a/src/test/scala/lesynth/util/TestConfig.scala
+++ /dev/null
@@ -1,42 +0,0 @@
-package lesynth
-package util
-
-import java.util.logging.FileHandler
-import java.util.logging.Level
-import java.util.logging.SimpleFormatter
-
-import insynth.Config
-
-// used to configure global setting before tests are run
-object TestConfig {
-
-	// create a file handler with appropriate path (no appending)
-	val inSynthHandler = new FileHandler("insynthleon.txt", true);
-	// set to log all levels
-	inSynthHandler.setLevel(Level.ALL);
-	// set simple text formatter
-	inSynthHandler.setFormatter(new SimpleFormatter);
-	
-	Config.setLoggerHandler(inSynthHandler)
-  
-  val testDir = "testcases/insynth-leon-tests/" 
-    
-  val synthesisTestDir = "testcases/insynth-synthesis-tests/" 
-    
-  val lesynthTestDir = "testcases/lesynth/test/" 
-    
-  val lesynthSynthesisDir = "testcases/lesynth/synthesis/"
-  
-  val HOME_FOLDER = "/home/kuraj/"
-    
-  val classpathArray = Array(
-    "target/scala-2.9.2/classes",
-    "library/target/scala-2.9.2/classes",
-    "unmanaged/64/cafebabe_2.9.2-1.2.jar",
-    "unmanaged/64/scalaz3.jar",
-    HOME_FOLDER + ".ivy2/cache/com.typesafe.akka/akka-actor/jars/akka-actor-2.0.4.jar",
-    HOME_FOLDER + ".ivy2/cache/com.typesafe/config/bundles/config-0.3.1.jar",    
-    HOME_FOLDER + ".sbt/boot/scala-2.9.2/lib/scala-library.jar",
-    HOME_FOLDER + ".sbt/boot/scala-2.9.2/lib/scala-compiler.jar"
-	)
-}
\ No newline at end of file
diff --git a/src/test/scala/lesynth/util/Scaffold.scala b/src/test/scala/util/Scaffold.scala
similarity index 78%
rename from src/test/scala/lesynth/util/Scaffold.scala
rename to src/test/scala/util/Scaffold.scala
index 218337fcd3ef9e01b9bbe4d20c9b05c47b16d6ab..fd31cdc20c47849fa5df22c856eded7f4e1bb35f 100644
--- a/src/test/scala/lesynth/util/Scaffold.scala
+++ b/src/test/scala/util/Scaffold.scala
@@ -1,4 +1,3 @@
-package lesynth
 package util
 
 import org.scalatest.FunSuite
@@ -7,6 +6,8 @@ import org.scalatest.matchers.ShouldMatchers._
 import java.io.{BufferedWriter, FileWriter, File}
 
 import leon._
+import leon.test._
+import leon.utils._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
 import leon.purescala.TreeOps._
@@ -17,8 +18,11 @@ import leon.synthesis.utils._
 
 object Scaffold {
 
+  val reporter = new TestSilentReporter
+
   def forProgram(content: String): Iterable[(SynthesisContext, FunDef, Problem)] = {
 
+    val forProgramReporter = new TestSilentReporter
     val ctx = LeonContext(
       settings = Settings(
         synthesis = true,
@@ -26,7 +30,8 @@ object Scaffold {
         verify    = false		
       ),
       files = List(),
-      reporter = new SilentReporter
+      reporter = forProgramReporter,
+      interruptManager = new InterruptManager(forProgramReporter)
     )
 //    Settings.showIDs = true
 
@@ -35,7 +40,7 @@ object Scaffold {
     val (program, results) = try {
       pipeline.run(ctx)((content, Nil))
     } catch {
-      case _ =>
+      case _: Throwable =>
         fail("Error while processing")
     }
     
@@ -44,15 +49,17 @@ object Scaffold {
 
   def forFile(file: String): Iterable[(SynthesisContext, FunDef, Problem)] = {
     val programFile = new File(file)
-    
+
+    val forProgramReporter = new TestSilentReporter
     val ctx = LeonContext(
       settings = Settings(
         synthesis = true,
         xlang     = false,
-        verify    = false		
+        verify    = false
       ),
       files = List(programFile),
-      reporter = new SilentReporter
+      reporter = forProgramReporter,
+      interruptManager = new InterruptManager(forProgramReporter)
     )
 
     val pipeline = leon.plugin.ExtractionPhase andThen SynthesisProblemExtractionPhase
@@ -60,7 +67,7 @@ object Scaffold {
     val (program, results) = try {
       pipeline.run(ctx)(file :: Nil)
     } catch {
-      case _ =>
+      case _: Throwable =>
         fail("Error while processing " + file)
     }
     
@@ -71,12 +78,6 @@ object Scaffold {
     problemMap: Map[leon.purescala.Definitions.FunDef,Seq[leon.synthesis.Problem]]) = {
 
     val opts = SynthesisOptions()
-    
-    val solver = new FairZ3Solver(ctx)
-    solver.setProgram(program)
-
-    val simpleSolver = new UninterpretedZ3Solver(ctx)
-    simpleSolver.setProgram(program)
 
     for ((f, ps) <- problemMap; p <- ps) 
     	yield {
@@ -84,13 +85,10 @@ object Scaffold {
                                     opts,
                                     Some(f),
                                     program,
-                                    solver,
-                                    simpleSolver,
-                                    new SilentReporter,
-                                    new java.util.concurrent.atomic.AtomicBoolean)
+                                    new TestSilentReporter)
 
         (sctx, f, p)
     	}
   }
   
-}
\ No newline at end of file
+}
diff --git a/src/test/scala/lesynth/util/Utils.scala b/src/test/scala/util/Utils.scala
similarity index 98%
rename from src/test/scala/lesynth/util/Utils.scala
rename to src/test/scala/util/Utils.scala
index 56fb6c6e489ae24ade4ddba5281734d11b3f5a15..dd72243f09fd3628a5b1169343c3e03ba6bc29aa 100644
--- a/src/test/scala/lesynth/util/Utils.scala
+++ b/src/test/scala/util/Utils.scala
@@ -1,4 +1,3 @@
-package lesynth
 package util
 
 import org.scalatest.FunSuite
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
similarity index 100%
rename from testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
rename to testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
similarity index 100%
rename from testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
rename to testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
diff --git a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
similarity index 100%
rename from testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
rename to testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala
rename to testcases/condabd/benchmarks/BatchedQueue/BatchedQueue.scala
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
rename to testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala
rename to testcases/condabd/benchmarks/BatchedQueue/BatchedQueueFull.scala
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
rename to testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala
rename to testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
rename to testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
diff --git a/testcases/lesynth/synthesis/BinarySearch.scala b/testcases/condabd/benchmarks/BinarySearch.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BinarySearch.scala
rename to testcases/condabd/benchmarks/BinarySearch.scala
diff --git a/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala
rename to testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeFull.scala
diff --git a/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
similarity index 100%
rename from testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala
rename to testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
diff --git a/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala b/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
similarity index 100%
rename from testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala
rename to testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
diff --git a/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala b/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
similarity index 100%
rename from testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala
rename to testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
diff --git a/testcases/lesynth/synthesis/List/ListConcat.scala b/testcases/condabd/benchmarks/List/ListConcat.scala
similarity index 100%
rename from testcases/lesynth/synthesis/List/ListConcat.scala
rename to testcases/condabd/benchmarks/List/ListConcat.scala
diff --git a/testcases/lesynth/synthesis/List/ListSearch.scala b/testcases/condabd/benchmarks/List/ListSearch.scala
similarity index 100%
rename from testcases/lesynth/synthesis/List/ListSearch.scala
rename to testcases/condabd/benchmarks/List/ListSearch.scala
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
similarity index 100%
rename from testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala
rename to testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
similarity index 100%
rename from testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
rename to testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
similarity index 100%
rename from testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala
rename to testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
diff --git a/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
similarity index 100%
rename from testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala
rename to testcases/condabd/benchmarks/RedBlackTree/RedBlackTree.scala
diff --git a/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
similarity index 100%
rename from testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala
rename to testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
diff --git a/testcases/lesynth/test/Addresses.scala b/testcases/condabd/test/insynth/Addresses.scala
similarity index 100%
rename from testcases/lesynth/test/Addresses.scala
rename to testcases/condabd/test/insynth/Addresses.scala
diff --git a/testcases/condabd/test/insynth/AddressesWithAddition.scala b/testcases/condabd/test/insynth/AddressesWithAddition.scala
new file mode 100644
index 0000000000000000000000000000000000000000..04a73ae087b993d61fc9e43b73c64f7ee2247bc9
--- /dev/null
+++ b/testcases/condabd/test/insynth/AddressesWithAddition.scala
@@ -0,0 +1,52 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object AddressesWithAddition {
+  
+  case class Address(aComp: Int, bComp: Int, priv: Boolean)
+  
+  sealed abstract class List
+  case class Cons(a: Address, tail:List) extends List
+  case object Nil extends List
+
+  def setA(l: List) : Set[Address] = l match {
+    case Nil => Set.empty[Address]
+    case Cons(a, l1) => Set(a) ++ setA(l1)
+  }
+  
+	def size(l: List) : Int = l match {
+	  case Nil => 0
+	  case Cons(head, tail) => 1 + size(tail)
+	}
+	
+  def allPrivate(l: List): Boolean = l match {
+    case Nil => true
+    case Cons(a, l1) =>
+      if (a.priv) allPrivate(l1)
+      else false
+  }
+	
+  def allBusiness(l: List): Boolean = l match {
+    case Nil => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook(business : List, pers : List)
+  
+  def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+  
+  def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+  
+  def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+  	  
+  def makeAddressBook(l: List, x: Int, y: Boolean): AddressBook = 
+		choose {
+    (res: AddressBook) =>
+		  size(res) == size(l) &&
+		  allPrivate(res.pers) && allBusiness(res.business)
+  }
+  
+}
diff --git a/testcases/lesynth/test/refinement/ListConcat.scala b/testcases/condabd/test/insynth/ListConcat.scala
similarity index 99%
rename from testcases/lesynth/test/refinement/ListConcat.scala
rename to testcases/condabd/test/insynth/ListConcat.scala
index 96a2d909ac25e11596ee86c63d884df08d5be7e3..20972e8af864cc1a618fe5d74278ce4298c01c35 100644
--- a/testcases/lesynth/test/refinement/ListConcat.scala
+++ b/testcases/condabd/test/insynth/ListConcat.scala
@@ -3,6 +3,7 @@ import scala.collection.immutable.Set
 import leon.Utils._
 
 object ListOperations {
+
     sealed abstract class List
     case class Cons(head: Int, tail: List) extends List
     case class Nil() extends List
diff --git a/testcases/lesynth/test/AddressesMergeAddressBooks.scala b/testcases/condabd/test/lesynth/Addresses.scala
similarity index 64%
rename from testcases/lesynth/test/AddressesMergeAddressBooks.scala
rename to testcases/condabd/test/lesynth/Addresses.scala
index d308ac24746f388ab21c8f767bf5ffe1de215243..52260559cecdabef594aa208096cd9a05b93dbe5 100644
--- a/testcases/lesynth/test/AddressesMergeAddressBooks.scala
+++ b/testcases/condabd/test/lesynth/Addresses.scala
@@ -4,7 +4,7 @@ import leon.Utils._
 
 object Addresses {
   
-  case class Address(a: Int, b: Int, priv: Boolean)
+  case class Address(aComp: Int, bComp: Int, priv: Boolean)
   
   sealed abstract class List
   case class Cons(a: Address, tail:List) extends List
@@ -41,30 +41,12 @@ object Addresses {
   def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
   
   def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
-  
-  def makeAddressBook(l: List): AddressBook = (l match {
-    case Nil => AddressBook(Nil, Nil)
-    case Cons(a, l1) => {
-      val res = makeAddressBook(l1)
-      if (a.priv) AddressBook(res.business, Cons(a, res.pers))
-      else AddressBook(Cons(a, res.business), res.pers)
-    }
-  }) ensuring {
+  	  
+  def makeAddressBook(l: List): AddressBook = 
+		choose {
     (res: AddressBook) =>
 		  size(res) == size(l) &&
 		  allPrivate(res.pers) && allBusiness(res.business)
   }
   
-  def merge(l1: List, l2: List): List = l1 match {
-    case Nil => l2
-    case Cons(a, tail) => Cons(a, merge(tail, l2))
-  }
-  
-  def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = 
-		choose {
-    (res: AddressBook) =>
-		  size(res) == size(ab1) + size(ab2) &&
-		  allPrivate(res.pers) && allBusiness(res.business)
-  	}
-  
 }
diff --git a/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala b/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0d6d8c0677806c687186184aa929e80032b869a8
--- /dev/null
+++ b/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
@@ -0,0 +1,81 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+  case class Info(
+    address: Int,
+    zipcode: Int,
+    phoneNumber: Int
+  )
+  
+  case class Address(info: Info, priv: Boolean)
+  
+  sealed abstract class List
+  case class Cons(a: Address, tail:List) extends List
+  case object Nil extends List
+
+  def content(l: List) : Set[Address] = l match {
+    case Nil => Set.empty[Address]
+    case Cons(addr, l1) => Set(addr) ++ content(l1)
+  }
+  
+	def size(l: List) : Int = l match {
+	  case Nil => 0
+	  case Cons(head, tail) => 1 + size(tail)
+	}
+	
+  def allPrivate(l: List): Boolean = l match {
+    case Nil => true
+    case Cons(a, l1) =>
+      if (a.priv) allPrivate(l1)
+      else false
+  }
+	
+  def allBusiness(l: List): Boolean = l match {
+    case Nil => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook(business : List, pers : List)
+  
+  def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+  	  
+  	  def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+  	  
+  	  def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+  	    		 
+  def isEmpty(ab: AddressBook) = size(ab) == 0
+  
+  def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+  
+  def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+  
+  def makeAddressBook(l: List): AddressBook = (l match {
+    case Nil => AddressBook(Nil, Nil)
+    case Cons(a, l1) => {
+      val res = makeAddressBook(l1)
+      if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+      else AddressBook(Cons(a, res.business), res.pers)
+    }
+  }) ensuring {
+    (res: AddressBook) =>
+		  size(res) == size(l) && addressBookInvariant(res)
+  }
+  
+  def merge(l1: List, l2: List): List = l1 match {
+    case Nil => l2
+    case Cons(a, tail) => Cons(a, merge(tail, l2))
+  }
+  
+  def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = { 
+    require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+		choose {
+    (res: AddressBook) =>
+		  (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
+  	}
+  }
+  
+}
diff --git a/testcases/lesynth/test/verifier/BinarySearchTree.scala b/testcases/condabd/test/lesynth/BinarySearchTree.scala
similarity index 100%
rename from testcases/lesynth/test/verifier/BinarySearchTree.scala
rename to testcases/condabd/test/lesynth/BinarySearchTree.scala
diff --git a/testcases/condabd/test/lesynth/InsertionSortInsert.scala b/testcases/condabd/test/lesynth/InsertionSortInsert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ac832856ed117c3a7e68eabae2f5ab87b70ef3bb
--- /dev/null
+++ b/testcases/condabd/test/lesynth/InsertionSortInsert.scala
@@ -0,0 +1,61 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+  sealed abstract class List
+  case class Cons(head:Int,tail:List) extends List
+  case class Nil() extends List
+
+  def size(l : List) : Int = (l match {
+    case Nil() => 0
+    case Cons(_, xs) => 1 + size(xs)
+  }) ensuring(_ >= 0)
+
+  def contents(l: List): Set[Int] = l match {
+    case Nil() => Set.empty
+    case Cons(x,xs) => contents(xs) ++ Set(x)
+  }
+
+  def isSorted(l: List): Boolean = l match {
+    case Nil() => true
+    case Cons(x, Nil()) => true
+    case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+  }   
+
+  /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+   * the expected content and size */
+  def sortedIns(e: Int, l: List): List = {
+    require(isSorted(l))    
+    choose { (res : List) =>
+      (	
+        contents(res) == contents(l) ++ Set(e) &&
+        isSorted(res) &&
+        size(res) == size(l) + 1
+      )
+    }
+//    val cond1: Boolean =  /*!*/
+//    l match {
+//      case Nil() =>  /*!*/ // Cons(e,Nil())
+//      case Cons(x,xs) =>
+//				val cond2: Boolean =  /*!*/
+//				if (x <= e)  /*!*/ // Cons(x,sortedIns(e, xs))
+//				else  /*!*/ // Cons(e, l)
+//    } 
+  } 
+//  ensuring(res => contents(res) == contents(l) ++ Set(e) 
+//                    && isSorted(res)
+//                    && size(res) == size(l) + 1
+//            )
+
+  /* Insertion sort yields a sorted list of same size and content as the input
+   * list */
+  def sort(l: List): List = (l match {
+    case Nil() => Nil()
+    case Cons(x,xs) => sortedIns(x, sort(xs))
+  }) ensuring(res => contents(res) == contents(l) 
+                     && isSorted(res)
+                     && size(res) == size(l)
+             )
+
+}
diff --git a/testcases/condabd/test/lesynth/ListConcat.scala b/testcases/condabd/test/lesynth/ListConcat.scala
new file mode 100644
index 0000000000000000000000000000000000000000..20972e8af864cc1a618fe5d74278ce4298c01c35
--- /dev/null
+++ b/testcases/condabd/test/lesynth/ListConcat.scala
@@ -0,0 +1,21 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+
+    sealed abstract class List
+    case class Cons(head: Int, tail: List) extends List
+    case class Nil() extends List
+
+	  def content(l: List) : Set[Int] = l match {
+	    case Nil() => Set.empty
+	    case Cons(head, tail) => Set(head) ++ content(tail)
+	  }
+    
+    def concat(l1: List, l2: List) : List = choose {
+    (out : List) =>
+      content(out) == content(l1) ++ content(l2)
+    }
+
+}
diff --git a/testcases/lesynth/test/verifier/ListConcat.scala b/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
similarity index 100%
rename from testcases/lesynth/test/verifier/ListConcat.scala
rename to testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
diff --git a/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala b/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
similarity index 100%
rename from testcases/lesynth/test/refinement/ListConcatWithEmpty.scala
rename to testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
diff --git a/testcases/condabd/test/lesynth/MergeSortSort.scala b/testcases/condabd/test/lesynth/MergeSortSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..987c538c4ab36dc9b378f03fc24592210bcbd62b
--- /dev/null
+++ b/testcases/condabd/test/lesynth/MergeSortSort.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+  sealed abstract class List
+  case class Cons(head : Int, tail : List) extends List
+  case class Nil() extends List
+
+  sealed abstract class PairAbs
+  case class Pair(fst : List, snd : List) extends PairAbs
+
+  def contents(l : List) : Set[Int] = l match {
+    case Nil() => Set.empty
+    case Cons(x,xs) => contents(xs) ++ Set(x)
+  }
+
+  def isSorted(l : List) : Boolean = l match {
+    case Nil() => true
+    case Cons(x,xs) => xs match {
+      case Nil() => true
+      case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+    }
+  }    
+
+  def size(list : List) : Int = list match {
+    case Nil() => 0
+    case Cons(x,xs) => 1 + size(xs)
+  }
+
+  def splithelper(aList : List, bList : List, n : Int) : Pair = {
+    if (n <= 0) Pair(aList,bList)
+    else
+	bList match {
+    	      case Nil() => Pair(aList,bList)
+    	      case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+	}
+  } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+//  def split(list : List, n : Int): Pair = {
+//    splithelper(Nil(),list,n)
+//  } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+  
+  def split(list: List): Pair = {
+    splithelper(Nil(),list,size(list)/2)
+  } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+  def merge(aList : List, bList : List) : List = {
+    require(isSorted(aList) && isSorted(bList))
+    bList match {       
+      case Nil() => aList
+      case Cons(x,xs) =>
+        aList match {
+              case Nil() => bList
+              case Cons(y,ys) =>
+               if (y < x)
+                  Cons(y,merge(ys, bList))
+               else
+                  Cons(x,merge(aList, xs))               
+        }   
+    }
+  } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+  def isEmpty(list: List) : Boolean = list match {
+    case Nil() => true
+    case Cons(x,xs) => false
+  }
+  
+  def sort(list : List) : List = choose {
+      
+    (res : List) =>
+      contents(res) == contents(list) && isSorted(res)
+      
+//      list match {
+//    case Nil() => list
+//    case Cons(x,Nil()) => list
+//    case _ =>
+//    	 val p = split(list,size(list)/2)
+//   	 merge(mergeSort(p.fst), mergeSort(p.snd))
+      
+//      merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+  }
+  
+  //ensuring(res => contents(res) == contents(list) && isSorted(res))
+ 
+}
diff --git a/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala b/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e6413ffaf8278fdacb43372eb615ced566e60022
--- /dev/null
+++ b/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
@@ -0,0 +1,77 @@
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+  sealed abstract class Color
+  case class Red() extends Color
+  case class Black() extends Color
+
+  sealed abstract class Tree
+  case class 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)
+  }
+
+  def balance(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))
+      case Node(c, a, xV, b) => Node(c, a, xV, b)
+    }
+  } ensuring (res => content(res) == content(Node(c, a, x, b)))
+
+  // <<insert element x into the tree t>>
+  def ins(x: Int, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+    choose { (res: Tree) =>
+      content(res) == content(t) ++ Set(x) &&
+      size (t) <= size(res) && size(res) <= size(t) + 1 &&
+      redDescHaveBlackChildren (res) &&
+      blackBalanced (res)
+    }
+  }
+
+}
\ No newline at end of file
diff --git a/unmanaged/32/insynth_2.10-2.1.jar b/unmanaged/32/insynth_2.10-2.1.jar
new file mode 120000
index 0000000000000000000000000000000000000000..49be391b699bbe7d8f1f4b004e3be9633cefe4f4
--- /dev/null
+++ b/unmanaged/32/insynth_2.10-2.1.jar
@@ -0,0 +1 @@
+../common/insynth_2.10-2.1.jar
\ No newline at end of file
diff --git a/unmanaged/64/insynth_2.10-2.1.jar b/unmanaged/64/insynth_2.10-2.1.jar
new file mode 120000
index 0000000000000000000000000000000000000000..49be391b699bbe7d8f1f4b004e3be9633cefe4f4
--- /dev/null
+++ b/unmanaged/64/insynth_2.10-2.1.jar
@@ -0,0 +1 @@
+../common/insynth_2.10-2.1.jar
\ No newline at end of file
diff --git a/unmanaged/common/insynth_2.10-2.1.jar b/unmanaged/common/insynth_2.10-2.1.jar
new file mode 100644
index 0000000000000000000000000000000000000000..f277295b02f2e047f73b9d4e26c6d2baba4cc1c1
Binary files /dev/null and b/unmanaged/common/insynth_2.10-2.1.jar differ