diff --git a/src/main/scala/lesynth/Report.scala b/src/main/scala/leon/synthesis/condabd/Report.scala
similarity index 98%
rename from src/main/scala/lesynth/Report.scala
rename to src/main/scala/leon/synthesis/condabd/Report.scala
index 372784d032cd6504e853f3c40f147d699d567e24..caf0124592c8db3c09cc5f3b39e2cd54d3e56f16 100755
--- a/src/main/scala/lesynth/Report.scala
+++ b/src/main/scala/leon/synthesis/condabd/Report.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
diff --git a/src/main/scala/lesynth/SynthesisInfo.scala b/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
similarity index 98%
rename from src/main/scala/lesynth/SynthesisInfo.scala
rename to src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
index e438d247173037cb93e6f170b5c54f55bf3bdd55..e4825a16667e5439f24fd279f6a5bf388c5e952e 100644
--- a/src/main/scala/lesynth/SynthesisInfo.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesisInfo.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
import leon.StopwatchCollections
diff --git a/src/main/scala/lesynth/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
similarity index 99%
rename from src/main/scala/lesynth/SynthesizerExamples.scala
rename to src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
index a66557c4ddcdb473bb24112666df2c8b1a81efd8..beea692e621f44d5f553052786ccaead7e1a2f0f 100755
--- a/src/main/scala/lesynth/SynthesizerExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
import scala.collection.mutable.{ PriorityQueue, ArrayBuffer, HashSet }
@@ -20,17 +20,20 @@ import leon.evaluators.EvaluationResults
import leon.evaluators._
import leon.synthesis.{ Problem, SynthesisContext }
-import insynth.{ Solver => _, _ }
+import insynth._
import insynth.leon.loader._
import insynth.leon.{ LeonDeclaration => Declaration, _ }
-import insynth.engine._
import insynth.reconstruction.Output
-import insynth.util.logging.HasLogger
-import lesynth.examples._
-import lesynth.evaluation._
-import lesynth.ranking._
-import lesynth.refinement._
+import _root_.insynth.{ Solver => _, _ }
+import _root_.insynth.engine._
+import _root_.insynth.util.logging.HasLogger
+
+import examples._
+import evaluation._
+import ranking._
+import refinement._
+import verification._
import SynthesisInfo._
import SynthesisInfo.Action._
diff --git a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
similarity index 97%
rename from src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
index a24e93558751b8149cbdeb7bed959b37703cd085..d6fd0911c982cf88c3dfe72218208ebdba17a725 100644
--- a/src/main/scala/lesynth/evaluation/CodeGenExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/CodeGenExampleRunner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import scala.collection.mutable.ArrayBuffer
@@ -12,10 +12,10 @@ import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
import leon.codegen.CodeGenEvalParams
-import lesynth.examples._
-import lesynth.ranking._
+import examples._
+import ranking._
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
case class CodeGenExampleRunner(program: Program, funDef: FunDef, ctx: LeonContext,
candidates: Seq[Candidate], inputExamples: Seq[Example],
diff --git a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
similarity index 95%
rename from src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
index 45a22e5582c94fc211bbcb2aa68d3f85c960be13..e6930d7b5ba86749e2fb5c8ef6c66e6475af6804 100644
--- a/src/main/scala/lesynth/evaluation/DefaultExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/DefaultExampleRunner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import scala.collection.mutable.ArrayBuffer
@@ -11,10 +11,10 @@ import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
-import lesynth.examples._
-import lesynth.ranking._
+import examples._
+import ranking._
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
case class DefaultExampleRunner(program: Program, funDef: FunDef, ctx: LeonContext,
candidates: Seq[Candidate], inputExamples: Seq[Example],
diff --git a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
similarity index 97%
rename from src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
index 36ed41c3cb086ca169f8c17edf93beb0db2225fc..1ab73543a6a7c77f972f90856bd6496591286436 100644
--- a/src/main/scala/lesynth/evaluation/EvaluationStrategy.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/EvaluationStrategy.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import leon._
@@ -11,10 +11,10 @@ import leon.purescala.TreeOps
import leon.codegen.CodeGenEvalParams
import insynth.reconstruction.Output
-import insynth.util.logging._
+import _root_.insynth.util.logging._
-import lesynth.ranking._
-import lesynth.examples._
+import ranking._
+import examples._
trait EvaluationStrategy extends HasLogger {
def getRanker(candidatePairs: IndexedSeq[(Output)], bodyBuilder: (Expr) => Expr, inputExamples: Seq[Example]): Ranker
diff --git a/src/main/scala/lesynth/evaluation/ExampleRunner.scala b/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
similarity index 91%
rename from src/main/scala/lesynth/evaluation/ExampleRunner.scala
rename to src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
index c93a8fa9911fbf30fe7af40ed3b378ae883903ac..b57e1bd07d8ecd29ae686380c4d9ef5db1226c8e 100644
--- a/src/main/scala/lesynth/evaluation/ExampleRunner.scala
+++ b/src/main/scala/leon/synthesis/condabd/evaluation/ExampleRunner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package evaluation
import scala.collection.mutable.ArrayBuffer
@@ -8,9 +8,9 @@ import leon.purescala.Common.Identifier
import leon.evaluators._
import leon.evaluators.EvaluationResults.Result
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
-import lesynth.examples.Example
+import examples.Example
abstract class ExampleRunner(inputExamples: Seq[Example]) extends HasLogger {
diff --git a/src/main/scala/lesynth/examples/Example.scala b/src/main/scala/leon/synthesis/condabd/examples/Example.scala
similarity index 87%
rename from src/main/scala/lesynth/examples/Example.scala
rename to src/main/scala/leon/synthesis/condabd/examples/Example.scala
index 10a47e48c8b75512acf6ca74105769b0cf112c6d..2a9abdb5fce2899c3863df4bb122b3bbb6fae933 100644
--- a/src/main/scala/lesynth/examples/Example.scala
+++ b/src/main/scala/leon/synthesis/condabd/examples/Example.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package examples
import leon.purescala.Trees._
diff --git a/src/main/scala/lesynth/examples/InputExamples.scala b/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
similarity index 99%
rename from src/main/scala/lesynth/examples/InputExamples.scala
rename to src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
index 9336f53373dbe3cd2f5b802acc3850d5e78d75e3..d4732049c8539223080286895b3b92935b633145 100755
--- a/src/main/scala/lesynth/examples/InputExamples.scala
+++ b/src/main/scala/leon/synthesis/condabd/examples/InputExamples.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package examples
import leon.purescala.TypeTrees._
diff --git a/src/main/scala/insynth/InSynth.scala b/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
similarity index 89%
rename from src/main/scala/insynth/InSynth.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
index 3646bad45635882b50c8fbb58d631688a5b60f6e..5dea8c9a89cd11b1437387f11566ddfa72adb2a5 100644
--- a/src/main/scala/insynth/InSynth.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/InSynth.scala
@@ -1,14 +1,15 @@
-package insynth
+package leon.synthesis.condabd.insynth
-import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
-import insynth.reconstruction.codegen.CodeGenerator
-import insynth.reconstruction.Reconstructor
+import reconstruction.codegen.CodeGenerator
+import reconstruction.Reconstructor
+import insynth.reconstruction.stream.{ OrderedStreamFactory, UnorderedStreamFactory }
+import insynth.Solver
import insynth.engine.InitialEnvironmentBuilder
-import insynth.leon.{ LeonDeclaration => Declaration }
-import insynth.leon.loader.LeonLoader
-import insynth.leon.LeonQueryBuilder
+import leon.{ LeonDeclaration => Declaration }
+import leon.loader.LeonLoader
+import leon.query.LeonQueryBuilder
import _root_.leon.purescala.Definitions.Program
import _root_.leon.purescala.TypeTrees.{ TypeTree => Type }
diff --git a/src/main/scala/insynth/leon/CommonTypes.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
similarity index 89%
rename from src/main/scala/insynth/leon/CommonTypes.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
index 1e7f5ba6259a32ac1c6bb33874af87bbdd051e66..50c78fac03184df7bad4dddf70432da64f604710 100644
--- a/src/main/scala/insynth/leon/CommonTypes.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/CommonTypes.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
diff --git a/src/main/scala/insynth/leon/DomainTypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
similarity index 97%
rename from src/main/scala/insynth/leon/DomainTypeTransformer.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
index 7c37f3322beaa68fdbb15bda390223884d6efbd5..1ff79a4f9639ff0fa0fb84000bd778a06acc84f2 100644
--- a/src/main/scala/insynth/leon/DomainTypeTransformer.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/DomainTypeTransformer.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures._
diff --git a/src/main/scala/insynth/leon/LeonDeclaration.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
similarity index 97%
rename from src/main/scala/insynth/leon/LeonDeclaration.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
index 229b18395916d8106a32c5e94447c8f2897c5c08..ec910fcc0ec5dc2e02d0e716c9eb8fef3b255111 100644
--- a/src/main/scala/insynth/leon/LeonDeclaration.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/LeonDeclaration.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures.SuccinctType
import insynth.structures.Weight._
diff --git a/src/main/scala/insynth/leon/ReconstructionExpression.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
similarity index 97%
rename from src/main/scala/insynth/leon/ReconstructionExpression.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
index 3d9692e45af10dc9b2b1f169a61ef18596bff795..67db5ee3233d86d87871ae182ab5d4f401abee9c 100644
--- a/src/main/scala/insynth/leon/ReconstructionExpression.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/ReconstructionExpression.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import leon.purescala.TypeTrees.{ TypeTree => LeonType }
import leon.purescala.Trees.Expr
diff --git a/src/main/scala/insynth/leon/TypeTransformer.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
similarity index 97%
rename from src/main/scala/insynth/leon/TypeTransformer.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
index e22d48ba8123fcdba4c77d84ae0ac4d54bb5a89e..9ddff7a91c6301ec1f706f667cb2cbebaf1e79ad 100644
--- a/src/main/scala/insynth/leon/TypeTransformer.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/TypeTransformer.scala
@@ -1,4 +1,4 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
import insynth.structures._
diff --git a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
similarity index 94%
rename from src/main/scala/insynth/leon/loader/DeclarationFactory.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
index 809de1141df485de7a66c6ce85cdcea78bead39e..27e1294e53c3d1d767d406ec77d8ccd64091223d 100644
--- a/src/main/scala/insynth/leon/loader/DeclarationFactory.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/DeclarationFactory.scala
@@ -1,9 +1,10 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
+
+import leon.synthesis.condabd.insynth.leon.{ LeonDeclaration => Declaration, _ }
+import leon.synthesis.condabd.insynth.leon.TypeTransformer
-import insynth.leon.{ LeonDeclaration => Declaration, _ }
import insynth.engine.InitialEnvironmentBuilder
import insynth.structures.{ SuccinctType => InSynthType, Variable => InSynthVariable, _ }
-import insynth.leon.TypeTransformer
import leon.purescala.Definitions._
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
diff --git a/src/main/scala/insynth/leon/loader/LoadSpec.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
similarity index 56%
rename from src/main/scala/insynth/leon/loader/LoadSpec.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
index 835e1f8fc9412b917d4444efc10f1a39a42beaee..2bd618183b9bc3eb8d4d6048807e05cf5b38a014 100644
--- a/src/main/scala/insynth/leon/loader/LoadSpec.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/LoadSpec.scala
@@ -1,4 +1,4 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
/** defines what to load in the PreLoader */
class LoadSpec {
diff --git a/src/main/scala/insynth/leon/loader/Loader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
similarity index 97%
rename from src/main/scala/insynth/leon/loader/Loader.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
index 5a7a9080580ca02aa08f5d0987cd4467a5e56f93..f703f8ae0534be848c74c43c76b27776b3f513c8 100644
--- a/src/main/scala/insynth/leon/loader/Loader.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/Loader.scala
@@ -1,6 +1,6 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
-import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
+import leon.synthesis.condabd.insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression, ImmediateExpression, UnaryReconstructionExpression }
import insynth.structures.{ SuccinctType => InSynthType }
import insynth.load.Loader
import insynth.util.logging.HasLogger
diff --git a/src/main/scala/insynth/leon/loader/PreLoader.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
similarity index 97%
rename from src/main/scala/insynth/leon/loader/PreLoader.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
index 2a1d6fe0a9ea24395ae1f8f27d091c3d5443bc46..47223b5a924d783a7380329cd2b40aa20394ced3 100644
--- a/src/main/scala/insynth/leon/loader/PreLoader.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/loader/PreLoader.scala
@@ -1,7 +1,9 @@
-package insynth.leon.loader
+package leon.synthesis.condabd.insynth.leon.loader
+import leon.synthesis.condabd.insynth.leon.{
+ LeonDeclaration => Declaration, NaryReconstructionExpression => NAE, ImmediateExpression => IE
+}
import insynth.structures.{ SuccinctType => InSynthType }
-import insynth.leon.{ LeonDeclaration => Declaration, NaryReconstructionExpression => NAE, ImmediateExpression => IE }
import insynth.engine.InitialEnvironmentBuilder
import leon.purescala.Definitions.{ Program, FunDef }
diff --git a/src/main/scala/insynth/leon/LeonQuery.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
similarity index 82%
rename from src/main/scala/insynth/leon/LeonQuery.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
index 9b4ba6d166c042f4da43a42a961815cfee94b2b5..f2947b60c355e9c843d6a192a870e0e1db6abbcf 100644
--- a/src/main/scala/insynth/leon/LeonQuery.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQuery.scala
@@ -1,6 +1,7 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
+package query
-import insynth.leon.loader.DeclarationFactory
+import loader.DeclarationFactory
import insynth.engine.InitialSender
import insynth.structures.SuccinctType
import insynth.query.Query
diff --git a/src/main/scala/insynth/leon/LeonQueryBuilder.scala b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
similarity index 89%
rename from src/main/scala/insynth/leon/LeonQueryBuilder.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
index e78ef6e7b63056e07c8a8b23c668940c190c4bb6..177240b41978503a6a02d170af259739cb321297 100644
--- a/src/main/scala/insynth/leon/LeonQueryBuilder.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/leon/query/LeonQueryBuilder.scala
@@ -1,10 +1,11 @@
-package insynth.leon
+package leon.synthesis.condabd.insynth.leon
+package query
import insynth.query._
import insynth.engine.InitialSender
import insynth.structures.{ SuccinctType, Const, Arrow, TSet }
-import insynth.leon.loader.DeclarationFactory
+import loader.DeclarationFactory
import leon.purescala.TypeTrees.{ TypeTree => LeonType, _ }
import leon.purescala.Common.FreshIdentifier
diff --git a/src/main/scala/insynth/reconstruction/Output.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
similarity index 87%
rename from src/main/scala/insynth/reconstruction/Output.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
index 0f0a13a999c38eaf0428138401c56675560d001e..d4929d82b1e5d5555752d95223bbe20869554954 100644
--- a/src/main/scala/insynth/reconstruction/Output.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Output.scala
@@ -1,4 +1,4 @@
-package insynth.reconstruction
+package leon.synthesis.condabd.insynth.reconstruction
import insynth.structures.Weight._
import leon.purescala.Trees.Expr
diff --git a/src/main/scala/insynth/reconstruction/Reconstructor.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
similarity index 89%
rename from src/main/scala/insynth/reconstruction/Reconstructor.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
index a1e6506c1f73a5ec78abf9dd6c4cc79a8e8211c5..389d50788e1d9f5f262e7e1729588bb25cf4941d 100644
--- a/src/main/scala/insynth/reconstruction/Reconstructor.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/Reconstructor.scala
@@ -1,9 +1,10 @@
-package insynth.reconstruction
+package leon.synthesis.condabd.insynth.reconstruction
import insynth.structures.{ SimpleNode, Weight }
import insynth.reconstruction.stream.{ Node => LambdaNode, _ }
+import insynth.reconstruction._
-import insynth.reconstruction.codegen.CodeGenerator
+import codegen.CodeGenerator
import insynth.util.format.{ FormatSuccinctNode, FormatStreamUtils }
import insynth.util.logging.HasLogger
diff --git a/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
similarity index 93%
rename from src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
rename to src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
index ae1f934415074fede778ba81279426f1a94eedda..0342dcc0d9ee5d661648416df0cb610b9c8a77ea 100644
--- a/src/main/scala/insynth/reconstruction/codegen/CodeGenerator.scala
+++ b/src/main/scala/leon/synthesis/condabd/insynth/reconstruction/codegen/CodeGenerator.scala
@@ -1,19 +1,19 @@
-package insynth.reconstruction.codegen
+package leon
+package synthesis.condabd.insynth
+package reconstruction.codegen
import scala.text.Document
import scala.text.Document.empty
-import insynth.leon._
+import leon._
import insynth.reconstruction.stream._
-
import insynth.structures.Function
-
import insynth.util.logging.HasLogger
-import leon.purescala.Trees.{ Expr }
-import leon.purescala.TypeTrees.{ TypeTree => DomainType, FunctionType }
-import leon.purescala.{ TypeTrees => domain }
-import leon.purescala.Trees.{ Expr => CodeGenOutput }
+import purescala.Trees.{ Expr }
+import purescala.TypeTrees.{ TypeTree => DomainType, FunctionType }
+import purescala.{ TypeTrees => domain }
+import purescala.Trees.{ Expr => CodeGenOutput }
/**
* class that converts an intermediate tree into a list of output elements (elements
diff --git a/src/main/scala/lesynth/ranking/Candidate.scala b/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
similarity index 96%
rename from src/main/scala/lesynth/ranking/Candidate.scala
rename to src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
index 761a0e2b3a5148e9601f4878115805338b9d7e1d..1c073f8797811236eecdc057065d8699c5068f9b 100644
--- a/src/main/scala/lesynth/ranking/Candidate.scala
+++ b/src/main/scala/leon/synthesis/condabd/ranking/Candidate.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package ranking
import leon.purescala.Trees._
@@ -8,8 +8,8 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps
import insynth.reconstruction.Output
-import insynth.structures.Weight._
-import insynth.util.logging.HasLogger
+import _root_.insynth.structures.Weight._
+import _root_.insynth.util.logging.HasLogger
object Candidate {
private var _freshResultVariable: Identifier = _
diff --git a/src/main/scala/lesynth/ranking/Evaluation.scala b/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
similarity index 97%
rename from src/main/scala/lesynth/ranking/Evaluation.scala
rename to src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
index 7186b689d37ebfc6eec45992253aa95c889c417d..88472e33d4aa461787492d5d3217dd126d881f0d 100644
--- a/src/main/scala/lesynth/ranking/Evaluation.scala
+++ b/src/main/scala/leon/synthesis/condabd/ranking/Evaluation.scala
@@ -1,7 +1,7 @@
-package lesynth
+package leon.synthesis.condabd
package ranking
-import lesynth.evaluation._
+import evaluation._
case class Evaluation(exampleRunner: ExampleRunner) {
diff --git a/src/main/scala/lesynth/ranking/Ranker.scala b/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
similarity index 99%
rename from src/main/scala/lesynth/ranking/Ranker.scala
rename to src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
index 39c4f753aeaaa58f80a0056aae3a03be8dde0695..3654b69e7be9b03b1ef5df2650b54b094f48ae5e 100644
--- a/src/main/scala/lesynth/ranking/Ranker.scala
+++ b/src/main/scala/leon/synthesis/condabd/ranking/Ranker.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package ranking
import scala.util.control.Breaks._
diff --git a/src/main/scala/lesynth/refinement/Filter.scala b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
similarity index 98%
rename from src/main/scala/lesynth/refinement/Filter.scala
rename to src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
index 90c6f25dea44c56f3e1127af488fab65e421f3cf..b524d66a4788d412d4158e1aa1b7f5781d823caa 100755
--- a/src/main/scala/lesynth/refinement/Filter.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/Filter.scala
@@ -1,5 +1,5 @@
-package lesynth
-package refinement
+package leon.synthesis
+package condabd.refinement
import scala.collection.mutable._
@@ -10,7 +10,7 @@ import leon.purescala.Common.{ Identifier, FreshIdentifier }
import leon.purescala.TreeOps
import leon.plugin.ExtractionPhase
-import insynth.leon.loader.LeonLoader
+import condabd.insynth.leon.loader.LeonLoader
import insynth.util.logging.HasLogger
/**
diff --git a/src/main/scala/lesynth/refinement/VariableRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
similarity index 97%
rename from src/main/scala/lesynth/refinement/VariableRefiner.scala
rename to src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
index df821f62fad976b6b2461f1e0d21ab18a9b3afda..07c9ed8db774fd0c8154c67bd01268d1f61fdb0b 100755
--- a/src/main/scala/lesynth/refinement/VariableRefiner.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableRefiner.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package refinement
import scala.collection.mutable.{Map => MutableMap}
@@ -13,7 +13,7 @@ import leon.purescala.Common.{ Identifier, FreshIdentifier }
import insynth.leon.loader._
import insynth.leon.{ LeonDeclaration => Declaration, _ }
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
// each variable of super type can actually have a subtype
// get sine declaration maps to be able to refine them
diff --git a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
similarity index 91%
rename from src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
rename to src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
index 59ec68fcc9167c2bd6c2a878585b1286f59ec5ce..45adc6a242ddd3484871d60761eb65ea12fe2721 100755
--- a/src/main/scala/lesynth/refinement/VariableSolverRefiner.scala
+++ b/src/main/scala/leon/synthesis/condabd/refinement/VariableSolverRefiner.scala
@@ -1,23 +1,23 @@
-package lesynth
+package leon
+package synthesis.condabd
package refinement
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
-import leon._
-import leon.purescala.Extractors._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.Definitions._
-import leon.solvers._
-import leon.purescala.Common.{ Identifier, FreshIdentifier }
-import leon.synthesis.Problem
+import purescala.Extractors._
+import purescala.TypeTrees._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.Definitions._
+import purescala.Common.{ Identifier, FreshIdentifier }
+import solvers._
+import synthesis.Problem
import insynth.leon.loader._
import insynth.leon._
-import insynth.util.logging.HasLogger
+import _root_.insynth.util.logging.HasLogger
// each variable of super type can actually have a subtype
// get sine declaration maps to be able to refine them
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
similarity index 97%
rename from src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
rename to src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
index 5feec355e246589a57fc08e5d39f6fb5a8d55816..35eadb6b13575236ae07267069eefe33e34219e8 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisImmediate.scala
+++ b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisImmediate.scala
@@ -1,4 +1,4 @@
-//package lesynth
+//package leon.synthesis.condabd
//package rules
//
//import leon.purescala.Trees._
@@ -11,8 +11,8 @@
//import leon.solvers.{ Solver, TimeoutSolver }
//import leon.evaluators.CodeGenEvaluator
//
-//import lesynth.examples.InputExamples._
-//import lesynth.evaluation._
+//import examples.InputExamples._
+//import evaluation._
//
//import leon.StopwatchCollections
//
diff --git a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
similarity index 97%
rename from src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
rename to src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
index 95324fce673698bb056e3f5769b4dadcc995e1b5..21f63f6c4e61891062bb08dc25ac9823f78f2da1 100755
--- a/src/main/scala/lesynth/rules/ConditionAbductionSynthesisTwoPhase.scala
+++ b/src/main/scala/leon/synthesis/condabd/rules/ConditionAbductionSynthesisTwoPhase.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.synthesis.condabd
package rules
import leon.purescala.Trees._
@@ -11,8 +11,8 @@ import leon.synthesis._
import leon.solvers._
import leon.evaluators.CodeGenEvaluator
-import lesynth.examples.InputExamples._
-import lesynth.evaluation._
+import examples.InputExamples._
+import evaluation._
import leon.StopwatchCollections
diff --git a/src/main/scala/lesynth/verification/AbstractVerifier.scala b/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
similarity index 90%
rename from src/main/scala/lesynth/verification/AbstractVerifier.scala
rename to src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
index 0508293bbca94c0fb86e6eabb4b4b607175a7b12..b9922e25505f024ebdce30d4f0457505ce72e6e0 100644
--- a/src/main/scala/lesynth/verification/AbstractVerifier.scala
+++ b/src/main/scala/leon/synthesis/condabd/verification/AbstractVerifier.scala
@@ -1,18 +1,19 @@
-package lesynth
+package leon
+package synthesis
+package condabd
+package verification
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.synthesis._
+import solvers._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
-import insynth.util.logging._
+import _root_.insynth.util.logging._
-abstract class AbstractVerifier(solverf: SolverFactory[Solver], p: Problem,
- synthInfo: SynthesisInfo)
+abstract class AbstractVerifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo)
extends HasLogger {
val solver = solverf.getNewSolver
diff --git a/src/main/scala/lesynth/verification/RelaxedVerifier.scala b/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
similarity index 86%
rename from src/main/scala/lesynth/verification/RelaxedVerifier.scala
rename to src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
index 91d8b09466ab19ce58232e30ec90044b92ee19e3..2dfa8784349995a2f2dfba43ef1993ee683dc75e 100644
--- a/src/main/scala/lesynth/verification/RelaxedVerifier.scala
+++ b/src/main/scala/leon/synthesis/condabd/verification/RelaxedVerifier.scala
@@ -1,15 +1,17 @@
-package lesynth
+package leon
+package synthesis
+package condabd
+package verification
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.synthesis._
+import solvers._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
-import insynth.util.logging._
+import _root_.insynth.util.logging._
class RelaxedVerifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
diff --git a/src/main/scala/lesynth/verification/Verifier.scala b/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
similarity index 84%
rename from src/main/scala/lesynth/verification/Verifier.scala
rename to src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
index eda23f3f2abae1c32887503a194bcf3a9e69cfe0..c1c74a38a86a1fd6ccd6619422de6606ec07a5a1 100644
--- a/src/main/scala/lesynth/verification/Verifier.scala
+++ b/src/main/scala/leon/synthesis/condabd/verification/Verifier.scala
@@ -1,15 +1,17 @@
-package lesynth
+package leon
+package synthesis
+package condabd
+package verification
-import leon.solvers._
-import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.Extractors._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
-import leon.purescala.Definitions._
-import leon.synthesis._
+import solvers._
+import purescala.Common._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Definitions._
-import insynth.util.logging._
+import _root_.insynth.util.logging._
class Verifier(solverf: SolverFactory[Solver], p: Problem, synthInfo: SynthesisInfo = new SynthesisInfo)
extends AbstractVerifier(solverf, p, synthInfo) with HasLogger {
diff --git a/src/test/scala/lesynth/EvaluationTest.scala b/src/test/scala/leon/test/condabd/EvaluationTest.scala
similarity index 97%
rename from src/test/scala/lesynth/EvaluationTest.scala
rename to src/test/scala/leon/test/condabd/EvaluationTest.scala
index 59b04e930dcb345d9bba56e969b5117d6f9b70e2..ef7d53911fe434c75ac809968843666aadb7f2dd 100644
--- a/src/test/scala/lesynth/EvaluationTest.scala
+++ b/src/test/scala/leon/test/condabd/EvaluationTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import org.scalatest.FunSuite
import org.scalatest.matchers.ShouldMatchers._
@@ -14,13 +14,12 @@ import leon.codegen.CodeGenEvalParams
import leon.purescala.TypeTrees._
import leon.evaluators.EvaluationResults._
-import lesynth.examples.InputExamples
-import lesynth.evaluation.CodeGenEvaluationStrategy
-import lesynth.ranking.Candidate
-import insynth.reconstruction.Output
-import lesynth.examples.Example
+import leon.synthesis.condabd.examples._
+import leon.synthesis.condabd.evaluation.CodeGenEvaluationStrategy
+import leon.synthesis.condabd.ranking.Candidate
+import leon.synthesis.condabd.insynth.reconstruction.Output
-import _root_.util.Scaffold
+import util.Scaffold
// TODO codegen evaluator params should be used but not yet in master
class EvaluationTest extends FunSuite {
diff --git a/src/test/scala/lesynth/FilterTest.scala b/src/test/scala/leon/test/condabd/FilterTest.scala
similarity index 97%
rename from src/test/scala/lesynth/FilterTest.scala
rename to src/test/scala/leon/test/condabd/FilterTest.scala
index a308510fadd0c2fb9da17b0920b77d6c6655be25..d439df5363654401581941189d07c6af91b36d76 100644
--- a/src/test/scala/lesynth/FilterTest.scala
+++ b/src/test/scala/leon/test/condabd/FilterTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import scala.util.Random
@@ -6,17 +6,17 @@ import org.junit.Assert._
import org.junit.{ Test, Ignore, Before }
import org.scalatest.junit.JUnitSuite
-import insynth.leon.loader.LeonLoader
-import insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader.LeonLoader
+import leon.synthesis.condabd.insynth.leon._
import _root_.leon.purescala.Trees._
import _root_.leon.purescala.TypeTrees._
import _root_.leon.purescala._
import _root_.leon.purescala.Definitions._
-import lesynth.refinement._
+import leon.synthesis.condabd.refinement._
-import _root_.util._
+import util._
class FilterTest extends JUnitSuite {
diff --git a/src/test/scala/lesynth/VariableRefinerTest.scala b/src/test/scala/leon/test/condabd/VariableRefinerTest.scala
similarity index 95%
rename from src/test/scala/lesynth/VariableRefinerTest.scala
rename to src/test/scala/leon/test/condabd/VariableRefinerTest.scala
index dcaae9ee1a1a3ce262e570683069e8c39ff3633f..c6b9f43ad76c9c693090ea69b67af02631098bd0 100644
--- a/src/test/scala/lesynth/VariableRefinerTest.scala
+++ b/src/test/scala/leon/test/condabd/VariableRefinerTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import scala.util.Random
@@ -10,11 +10,10 @@ import leon.purescala.Common._
import leon.purescala.TypeTrees._
import leon.purescala.Trees._
-import insynth.leon._
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.refinement._
-import lesynth.refinement._
-
-import _root_.util.Scaffold._
+import util.Scaffold._
class VariableRefinerTest extends FunSpec with GivenWhenThen {
diff --git a/src/test/scala/lesynth/VariableSolverRefinerTest.scala b/src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
similarity index 97%
rename from src/test/scala/lesynth/VariableSolverRefinerTest.scala
rename to src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
index 52175cd08dc67ca8b63c21fb4dcf2bf1b76bdeae..dc1d945ca04ebbabe9914fe30415764a82aba6a5 100644
--- a/src/test/scala/lesynth/VariableSolverRefinerTest.scala
+++ b/src/test/scala/leon/test/condabd/VariableSolverRefinerTest.scala
@@ -1,4 +1,4 @@
-package lesynth
+package leon.test.condabd
import scala.util.Random
@@ -11,12 +11,11 @@ import leon.purescala.TypeTrees._
import leon.purescala.Trees._
import insynth._
-import insynth.leon._
-import insynth.leon.loader._
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.refinement._
-import lesynth.refinement._
-
-import _root_.util._
+import util._
class VariableSolverRefinerTest extends FunSpec with GivenWhenThen {
diff --git a/src/test/scala/lesynth/VerifierTest.scala b/src/test/scala/leon/test/condabd/VerifierTest.scala
similarity index 94%
rename from src/test/scala/lesynth/VerifierTest.scala
rename to src/test/scala/leon/test/condabd/VerifierTest.scala
index 7a41d0e76d982b1363a89b3bbdfb6a6a5a913211..de88e347cfaad3b941bc4b9bc38fdd1ffc6f3c12 100644
--- a/src/test/scala/lesynth/VerifierTest.scala
+++ b/src/test/scala/leon/test/condabd/VerifierTest.scala
@@ -1,21 +1,22 @@
-package lesynth
+package leon.test.condabd
import org.junit.Assert._
import org.junit._
import org.scalatest._
import org.scalatest.matchers._
-import insynth.leon.loader.LeonLoader
+import leon.synthesis.condabd.insynth.leon.loader.LeonLoader
+import leon.synthesis.condabd.verification._
-import _root_.leon.purescala._
-import _root_.leon.evaluators._
-import _root_.leon.solvers._
-import _root_.leon.purescala.Trees._
+import leon.purescala._
+import leon.evaluators._
+import leon.solvers._
+import leon.purescala.Trees._
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.synthesis.Problem
-import _root_.util._
+import util._
class VerifierTest extends FunSpec {
diff --git a/src/test/scala/lesynth/enumeration/EnumeratorTest.scala b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
similarity index 95%
rename from src/test/scala/lesynth/enumeration/EnumeratorTest.scala
rename to src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
index 6e54425f87f27e5f745e2527d084c47fcb56f902..fff9381c3565dc059ba8486fc39c7247fc3d58e8 100644
--- a/src/test/scala/lesynth/enumeration/EnumeratorTest.scala
+++ b/src/test/scala/leon/test/condabd/enumeration/EnumeratorTest.scala
@@ -1,15 +1,15 @@
-package lesynth
+package leon.test.condabd
-import insynth.InSynth
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
+import leon.synthesis.condabd.insynth.InSynth
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.insynth.reconstruction.codegen._
+import leon.synthesis.condabd.insynth.reconstruction.Output
-import insynth.reconstruction._
-import insynth.reconstruction.{ stream => lambda }
-import insynth.reconstruction.stream.{ OrderedStreamFactory }
-import insynth.reconstruction.codegen._
-import insynth.reconstruction.Output
+import _root_.insynth.engine._
+import _root_.insynth.reconstruction._
+import _root_.insynth.reconstruction.{ stream => lambda }
+import _root_.insynth.reconstruction.stream.{ OrderedStreamFactory }
import _root_.leon._
import _root_.leon.purescala._
@@ -17,20 +17,16 @@ import _root_.leon.purescala.Definitions._
import _root_.leon.purescala.Common._
import _root_.leon.purescala.TypeTrees._
import _root_.leon.purescala.Trees.{ Variable => LeonVariable, _ }
+import _root_.insynth.util.format._
+import _root_.insynth.util._
-import lesynth.refinement._
-//import lesynth.examples._
-//import lesynth.evaluation.CodeGenEvaluationStrategy
-//import lesynth.ranking.Candidate
+import leon.synthesis.condabd.refinement._
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 util._
import insynth.testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
diff --git a/src/test/scala/insynth/InSynthTest.scala b/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
similarity index 93%
rename from src/test/scala/insynth/InSynthTest.scala
rename to src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
index acf730adf28b246711457e9642eeefed463ea8f8..a7dee3aa7d0ec746c8927b6da879c274036e3459 100644
--- a/src/test/scala/insynth/InSynthTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/InSynthTest.scala
@@ -1,35 +1,30 @@
+package leon.test.condabd
package insynth
-import insynth.leon._
-import insynth.leon.loader._
-import insynth.engine._
+import leon.synthesis.condabd.insynth.InSynth
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
+import leon.synthesis.condabd.insynth.reconstruction.codegen._
+import leon.synthesis.condabd.insynth.reconstruction.Output
-import insynth.reconstruction._
-import insynth.reconstruction.{ stream => lambda }
-import insynth.reconstruction.stream.{ OrderedStreamFactory }
-import insynth.reconstruction.codegen._
-import insynth.reconstruction.Output
+import _root_.insynth.engine._
+import _root_.insynth.reconstruction._
+import _root_.insynth.reconstruction.{ stream => lambda }
+import _root_.insynth.reconstruction.stream.{ OrderedStreamFactory }
+import _root_.insynth.util.format._
+import _root_.insynth.util._
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 }
+import util._
+import testutil.{ CommonProofTrees, CommonDeclarations, CommonLambda }
// TODO test abstractions (vals)
class InSynthTest extends JUnitSuite {
diff --git a/src/test/scala/insynth/loader/LoaderTest.scala b/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
similarity index 96%
rename from src/test/scala/insynth/loader/LoaderTest.scala
rename to src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
index 5982957f78f699a20b46b529d307c8a2c322c4de..40f98eda82fd717cf05fd4467a50ed1d7d02e2b9 100644
--- a/src/test/scala/insynth/loader/LoaderTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/loader/LoaderTest.scala
@@ -1,10 +1,11 @@
+package leon.test.condabd
package insynth
package loader
-import _root_.util._
+import util._
-import insynth.leon._
-import insynth.leon.loader._
+import leon.synthesis.condabd.insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader._
import _root_.leon.purescala.Definitions._
import _root_.leon.purescala.Common._
diff --git a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala b/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
similarity index 89%
rename from src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
rename to src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
index 3d86a6fd81a32564f59cb9d6c26b491f64971509..c5a7f5bcbb27817d0b93c9b7fb80020eec79a9c0 100644
--- a/src/test/scala/insynth/reconstruction/CodeGeneratorTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/reconstruction/CodeGeneratorTest.scala
@@ -1,14 +1,15 @@
-package insynth.reconstruction
+package leon.test.condabd.insynth
+package reconstruction
import org.junit.Assert._
import org.junit.{ Test, Ignore }
import org.scalatest.junit.JUnitSuite
-import insynth.reconstruction.codegen.CodeGenerator
+import leon.synthesis.condabd.insynth.reconstruction.codegen.CodeGenerator
-import leon.purescala.Trees._
+import _root_.leon.purescala.Trees._
-import insynth.testutil.{ CommonLambda, CommonDeclarations }
+import testutil.{ CommonLambda, CommonDeclarations }
// NOTE function cannot return function in Leon, no need to test that
diff --git a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala b/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
similarity index 91%
rename from src/test/scala/insynth/reconstruction/ReconstructorTest.scala
rename to src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
index 177f2e01e61a82f6ead2e71a696c02d0c2747335..c57ef877e4428151282be6acb5a0d651968aaf5b 100644
--- a/src/test/scala/insynth/reconstruction/ReconstructorTest.scala
+++ b/src/test/scala/leon/test/condabd/insynth/reconstruction/ReconstructorTest.scala
@@ -1,17 +1,19 @@
-package insynth.reconstruction
+package leon.test.condabd.insynth
+package reconstruction
import org.junit.{ Test, Ignore, BeforeClass, AfterClass }
import org.junit.Assert._
import org.scalatest.junit.JUnitSuite
-import insynth.reconstruction.codegen.CodeGenerator
+import leon.synthesis.condabd.insynth.reconstruction.codegen.CodeGenerator
+import leon.synthesis.condabd.insynth.reconstruction._
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, CommonLeonExpressions, CommonUtils }
+import testutil.{ CommonProofTrees, CommonDeclarations, CommonLeonExpressions, CommonUtils }
class ReconstructorTest extends JUnitSuite {
diff --git a/src/test/scala/insynth/testutil/CommonDeclarations.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
similarity index 94%
rename from src/test/scala/insynth/testutil/CommonDeclarations.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
index faca9b3b27c5e1b0764877fe3a46b44f9a725fc5..8fb24261f795c2b4a142b43c7e859bce75ff8ff6 100644
--- a/src/test/scala/insynth/testutil/CommonDeclarations.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonDeclarations.scala
@@ -1,4 +1,4 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
@@ -6,8 +6,8 @@ import org.junit.Assert._
import org.junit.Test
import org.junit.Ignore
-import insynth.leon.loader.DeclarationFactory._
-import insynth.leon._
+import leon.synthesis.condabd.insynth.leon.loader.DeclarationFactory._
+import leon.synthesis.condabd.insynth.leon._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ FreshIdentifier }
diff --git a/src/test/scala/insynth/testutil/CommonLambda.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
similarity index 97%
rename from src/test/scala/insynth/testutil/CommonLambda.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
index e5dc73cb42a49da548bfcb03f0a96c40509bfb61..4ff98d9225ff8c47bf998e2064f89fee64e897b8 100644
--- a/src/test/scala/insynth/testutil/CommonLambda.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLambda.scala
@@ -1,6 +1,7 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
-import insynth.leon.{ LeonQueryBuilder => QueryBuilder, _ }
+import leon.synthesis.condabd.insynth.leon.query.{ LeonQueryBuilder => QueryBuilder, _ }
+import leon.synthesis.condabd.insynth.leon._
import insynth.reconstruction.stream._
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
diff --git a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
similarity index 95%
rename from src/test/scala/insynth/testutil/CommonLeonExpressions.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
index 1ab08d1b45f0cea2138f6dd56249a2c7e303381c..7576d3a08c1b5cf4c32b3ea8189250dd52df69eb 100644
--- a/src/test/scala/insynth/testutil/CommonLeonExpressions.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonLeonExpressions.scala
@@ -1,4 +1,4 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import leon.purescala.Definitions.{ FunDef, VarDecl, Program, ObjectDef }
import leon.purescala.Common.{ FreshIdentifier }
diff --git a/src/test/scala/insynth/testutil/CommonProofTrees.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
similarity index 97%
rename from src/test/scala/insynth/testutil/CommonProofTrees.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
index 82f5adac4ccdbca1ffbd40f039cab649429c19a1..2cf742e76d3f1297cc522b20c0c53ce5c8d61b2d 100644
--- a/src/test/scala/insynth/testutil/CommonProofTrees.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonProofTrees.scala
@@ -1,4 +1,4 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import scala.collection.mutable.{ Map => MutableMap, Set => MutableSet }
@@ -6,7 +6,7 @@ import org.junit.Assert._
import org.junit.Test
import org.junit.Ignore
-import insynth.leon.{ LeonQueryBuilder => QueryBuilder, _ }
+import leon.synthesis.condabd.insynth.leon.query.{ LeonQueryBuilder => QueryBuilder, _ }
import insynth.structures._
import leon.purescala.TypeTrees._
diff --git a/src/test/scala/insynth/testutil/CommonUtils.scala b/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
similarity index 82%
rename from src/test/scala/insynth/testutil/CommonUtils.scala
rename to src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
index 406452b93a799cb93b33108c113fb6e9649bcfa8..c0e9c24ae313170607e4998d838435c5a849f974 100644
--- a/src/test/scala/insynth/testutil/CommonUtils.scala
+++ b/src/test/scala/leon/test/condabd/insynth/testutil/CommonUtils.scala
@@ -1,8 +1,8 @@
-package insynth.testutil
+package leon.test.condabd.insynth.testutil
import org.junit.Assert._
-import insynth.reconstruction.Output
+import leon.synthesis.condabd.insynth.reconstruction.Output
object CommonUtils {
diff --git a/src/test/scala/util/Scaffold.scala b/src/test/scala/leon/test/condabd/util/Scaffold.scala
similarity index 98%
rename from src/test/scala/util/Scaffold.scala
rename to src/test/scala/leon/test/condabd/util/Scaffold.scala
index fd31cdc20c47849fa5df22c856eded7f4e1bb35f..253fc7054e0cbd5e3c90ae7be8b85fe23e3d569e 100644
--- a/src/test/scala/util/Scaffold.scala
+++ b/src/test/scala/leon/test/condabd/util/Scaffold.scala
@@ -1,3 +1,4 @@
+package leon.test.condabd
package util
import org.scalatest.FunSuite
diff --git a/src/test/scala/util/Utils.scala b/src/test/scala/leon/test/condabd/util/Utils.scala
similarity index 96%
rename from src/test/scala/util/Utils.scala
rename to src/test/scala/leon/test/condabd/util/Utils.scala
index dd72243f09fd3628a5b1169343c3e03ba6bc29aa..36c7ddf7d44143602c04c888bbe7747610a70c4d 100644
--- a/src/test/scala/util/Utils.scala
+++ b/src/test/scala/leon/test/condabd/util/Utils.scala
@@ -1,3 +1,4 @@
+package leon.test.condabd
package util
import org.scalatest.FunSuite