diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 4b54a38552d3c91dcaea8f6676cf65dfcc882cc6..acc1707eb8e8762c3ef5ad0ca1a3953a8dc4de0b 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -6,53 +6,14 @@ import purescala.TreeOps._
 import purescala.Definitions._
 
 object Extensions {
-  sealed abstract class Extension(reporter: Reporter) {
+  import leon.verification.{Analyser,Tactic}
+  import leon.solvers.Solver
+
+  abstract class Extension(reporter: Reporter) {
     def description: String
     def shortDescription: String = description
   }
 
-  abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
-    // This can be used by solvers to "see" the programs from which the
-    // formulas come. (e.g. to set up some datastructures for the defined
-    // ADTs, etc.) 
-    def setProgram(program: Program) : Unit = {}
-
-    // Returns Some(true) if valid, Some(false) if invalid,
-    // None if unknown.
-    // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
-    def solve(expression: Expr) : Option[Boolean]
-
-    def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty)
-
-    def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
-    def superseeds : Seq[String] = Nil
-
-    private var _forceStop = false
-    def halt() : Unit = {
-      _forceStop = true
-    }
-    def init() : Unit = {
-      _forceStop = false
-    }
-    protected def forceStop = _forceStop
-
-  }
-  
-  abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
-    // Does whatever the analysis should. Uses the reporter to
-    // signal results and/or errors.
-    def analyse(program: Program) : Unit
-  }
-
-  abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
-    def setProgram(program: Program) : Unit = {}
-    def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
-    def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
-    def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
-    def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
-    def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
-  }
-
   // The rest of the code is for dynamically loading extensions
 
   private var allLoaded : Seq[Extension] = Nil
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index f04a463cfe6dfaf969782c014a9cc344e72e012f..831b715db3beb67b5fa1e1c8be22bd4a52e1573f 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -13,7 +13,7 @@ object Main {
       /*FunctionHoisting,*/
       Simplificator,
       synthesis.SynthesisPhase,
-      AnalysisPhase
+      verification.AnalysisPhase
     )
   }
 
@@ -143,7 +143,7 @@ object Main {
 
     val pipeAnalysis: Pipeline[Program, Program] =
       if (settings.analyze) {
-        AnalysisPhase
+        verification.AnalysisPhase
       } else {
         NoopPhase[Program]()
       }
diff --git a/src/main/scala/leon/TestExtension.scala b/src/main/scala/leon/TestExtension.scala
deleted file mode 100644
index 5fd517280e6c00eb4939e0615a5b6d41f0822379..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/TestExtension.scala
+++ /dev/null
@@ -1,109 +0,0 @@
-package leon
-
-import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Extractors._
-import purescala.TypeTrees._
-import purescala.Definitions._
-import Extensions._
-
-class TestExtension(val reporter: Reporter) extends Analyser(reporter) {
-  val description : String = "Testing."
-  def analyse(program : Program) : Unit = {
-  }/*
-    for((f: FunDef) <- program.definedFunctions) {
-      reporter.info("Got an f ! " + f.id)
-      reporter.info("Normal  : " + f.body.get)
-      val iteized = matchToIfThenElse(expandLets(f.body.get))
-      reporter.info("ITEized : " + iteized)
-      reporter.info("Leadsto ? : " + (leadsToCall(iteized) : String))
-      cleanClausify(iteized, program)
-      val (e,l,m) = clausifyITE(iteized)
-      reporter.info("As clauses : " + e)
-      l.foreach(reporter.info(_))
-      reporter.info("***\n")
-    }
-    reporter.info("Done.")
-  }*/
-
-  type LiftedBoolean = Option[Boolean]
-  val Yes : LiftedBoolean  = Some(true)
-  val No : LiftedBoolean = Some(false)
-  val Maybe : LiftedBoolean = None
-  implicit def bool2liftedbool(b : Boolean) : LiftedBoolean = Some(b)
-  implicit def liftedbool2String(l : LiftedBoolean) : String = l match {
-    case Yes => "Yes"
-    case No => "No"
-    case Maybe => "Maybe"
-  }
-
-  // assumes no lets and no match.
-  def leadsToCall(e : Expr) : LiftedBoolean = e match {
-    case f : FunctionInvocation => true
-    case IfExpr(a1, a2, a3) => {
-      if(leadsToCall(a1) == Yes) Yes else (leadsToCall(a2),leadsToCall(a3)) match {
-        case (Yes,Yes) => Yes
-        case (No,No) => No
-        case _ => Maybe
-      }
-    }
-    case n @ NAryOperator(args, _) => {
-      val ra = args.map(leadsToCall(_))
-      if(ra.exists(_ == Yes)) {
-        Yes
-      } else if(ra.forall(_ == No)) {
-        No
-      } else {
-        Maybe
-      }
-    }
-    case b @ BinaryOperator(a1,a2,_) => (leadsToCall(a1),leadsToCall(a2)) match {
-      case (Yes,_) => Yes
-      case (_,Yes) => Yes
-      case (No,No) => No
-      case _ => Maybe
-    }
-    case u @ UnaryOperator(a,_) => leadsToCall(a)
-    case t : Terminal => false
-    case unhandled => scala.sys.error("unhandled.")
-  }
-
-  private def cleanClausify(formula : Expr, program : Program) : Unit = {
-    val nonRec = allNonRecursiveFunctionCallsOf(formula, program)
-    val allRec = functionCallsOf(formula) -- nonRec
-
-    val (e,l,m) = clausifyITE(formula)
-    var dangerSet : Set[Expr] = Set.empty[Expr] ++ allRec
-    var change : Boolean = true
-    var newSet : Set[Expr] = Set.empty
-
-    while(change) {
-      change = false
-    }
-  }
-
-  private def clausifyITE(formula : Expr) : (Expr, List[Expr], Map[Identifier,Identifier]) = {
-    var newClauses : List[Expr] = Nil
-    var ite2Bools : Map[Identifier,Identifier] = Map.empty
-
-    def clausify(ex : Expr) : Option[Expr] = ex match {
-      //case _ if leadsToCall(ex) == No => None
-      case ie @ IfExpr(cond, then, elze) => {
-        val switch = FreshIdentifier("path", true).setType(BooleanType).toVariable
-        val placeHolder = FreshIdentifier("iteval", true).setType(ie.getType).toVariable
-        newClauses = Iff(switch, cond) :: newClauses
-        newClauses = Implies(switch, Equals(placeHolder, then)) :: newClauses
-        newClauses = Implies(Not(switch), Equals(placeHolder, elze)) :: newClauses
-        // newBools = newBools + switch.id
-        ite2Bools = ite2Bools + (placeHolder.id -> switch.id)
-        Some(placeHolder)
-      }
-      case _ => None
-    }
-
-    val cleanedUp = searchAndReplaceDFS(clausify)(formula)
-
-    (cleanedUp, newClauses.reverse, ite2Bools)
-  }
-}
diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
index ac95c8095ec4a9af8543e8d0cecc795a5f8acd19..3db02146e338b8b6f72c886df9072c5d98f01311 100644
--- a/src/main/scala/leon/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -4,6 +4,8 @@ import leon.Extensions._
 import leon.Reporter
 import leon.Settings._
 
+import leon.verification.Analyser
+
 import leon.purescala.Common.Identifier
 import leon.purescala.Definitions._
 import leon.purescala.PrettyPrinter
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 5eb38b53677a2666f87e1f839314c45e61333aa9..699a5cb89438533a8701e730c105dbc48a860ad8 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1,7 +1,7 @@
 package leon
 package purescala
 
-import leon.Extensions.Solver
+import leon.solvers.Solver
 
 object TreeOps {
   import Common._
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d998013231be4548a885340fce579e39e09e40e9
--- /dev/null
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -0,0 +1,40 @@
+package leon
+package solvers
+
+import Extensions.Extension
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.TreeOps._
+import purescala.Trees._
+
+abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
+  // This can be used by solvers to "see" the programs from which the
+  // formulas come. (e.g. to set up some datastructures for the defined
+  // ADTs, etc.) 
+  // Ideally, we would pass it at construction time and not change it later.
+  def setProgram(program: Program) : Unit = {}
+
+  // Returns Some(true) if valid, Some(false) if invalid,
+  // None if unknown.
+  // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
+  def solve(expression: Expr) : Option[Boolean]
+
+  def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty)
+
+  def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
+  def superseeds : Seq[String] = Nil
+
+  private var _forceStop = false
+
+  def halt() : Unit = {
+    _forceStop = true
+  }
+
+  def init() : Unit = {
+    _forceStop = false
+  }
+
+  protected def forceStop = _forceStop
+}
+
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 5c31961fb2bc40e0d749e6b44112b74788e22b4a..414e8e1a4941f51659215e545b68095cdf1e30bc 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -15,7 +15,7 @@ import scala.collection.mutable.{Set => MutableSet}
 // This is just to factor out the things that are common in "classes that deal
 // with a Z3 instance"
 trait AbstractZ3Solver {
-  self: Solver =>
+  self: leon.solvers.Solver =>
 
   val reporter: Reporter
 
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 9d654c88fda3821b41765969de134acd28a50bbc..c229d44d3a81e1c4e1bbcf90ee94cc1657f807ba 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -2,6 +2,9 @@ package leon
 package solvers.z3
 
 import z3.scala._
+
+import leon.solvers.Solver
+
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Trees._
@@ -247,7 +250,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
       }
 
       reporter.info(" - Running Z3 search...")
-      val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
+      val answerModelCore : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
         // println(blockingSetAsZ3)
         z3.checkAssumptions(blockingSetAsZ3 : _*)
       } else {
@@ -259,6 +262,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
         z3SearchStopwatch.stop
         (a, m, Seq.empty[Z3AST])
       }
+      val (answer, model, core) = answerModelCore // to work around the stupid type inferer
+
       reporter.info(" - Finished search with blocked literals")
       Logger.debug("The blocking guards are: " + blockingSet.mkString(", "), 4, "z3solver")
 
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 1ad2ed1fc47f285d0b3ff3101b1c2698291a4958..0100286d6446b96173fa7e2c0b1d7b8d49ceeb9f 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -2,6 +2,9 @@ package leon
 package solvers.z3
 
 import z3.scala._
+
+import leon.solvers.Solver
+
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Trees._
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0dc4cb283f48c0674b8a3638a1e4f875f7e9affc..91ba9d37f14607bfd2ed867f750791cdbae5260d 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
 import purescala.Trees.{Expr, Not}
 import purescala.ScalaPrinter
 
-import Extensions.Solver
+import solvers.Solver
 import java.io.File
 
 import collection.mutable.PriorityQueue
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 5056ec0e8ead3156847a18a5f358cde951b11d5e..ea6ccabcb826289172607dc94bbf7398e8137716 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -1,5 +1,7 @@
 package leon.testgen
 
+import leon.verification.Analyser
+
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
diff --git a/src/main/scala/leon/verification/Analyser.scala b/src/main/scala/leon/verification/Analyser.scala
new file mode 100644
index 0000000000000000000000000000000000000000..84a2d87221bdfeb1d225ec6bb3542c2a5db7f4e4
--- /dev/null
+++ b/src/main/scala/leon/verification/Analyser.scala
@@ -0,0 +1,13 @@
+package leon
+package verification
+
+import Extensions.Extension
+
+import purescala.Definitions.Program
+
+// TODO this class is slowly but surely becoming useless, as we now have a notion of phases.
+abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
+  // Does whatever the analysis should. Uses the reporter to
+  // signal results and/or errors.
+  def analyse(program: Program) : Unit
+}
diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
similarity index 98%
rename from src/main/scala/leon/Analysis.scala
rename to src/main/scala/leon/verification/Analysis.scala
index e1fc9fb1f3fa155bc194433c2948a7fb2b1a34c0..94567233d6501e68adc1e0a3317d3aea80c29bcc 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -1,4 +1,5 @@
 package leon
+package verification
 
 import purescala.Common._
 import purescala.Definitions._
@@ -8,7 +9,7 @@ import purescala.TypeTrees._
 
 import Extensions._
 
-import solvers.TrivialSolver
+import solvers.{Solver,TrivialSolver}
 
 import scala.collection.mutable.{Set => MutableSet}
 
@@ -332,12 +333,3 @@ object Analysis {
     liftLets(Implies(And(trueThings.reverse), result))
   }
 }
-
-object AnalysisPhase extends UnitPhase[Program] {
-  val name = "Analysis"
-  val description = "Leon Analyses"
-
-  def apply(ctx: LeonContext, program: Program) {
-    new Analysis(program).analyse
-  }
-}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..69e35fe0bbab96804fd8703ecab3049bd1db9fad
--- /dev/null
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -0,0 +1,13 @@
+package leon
+package verification
+
+import purescala.Definitions._
+
+object AnalysisPhase extends UnitPhase[Program] {
+  val name = "Analysis"
+  val description = "Leon Analyses"
+
+  def apply(ctx: LeonContext, program: Program) {
+    new Analysis(program).analyse
+  }
+}
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
similarity index 99%
rename from src/main/scala/leon/DefaultTactic.scala
rename to src/main/scala/leon/verification/DefaultTactic.scala
index 4078e6e490f8a1bbe5adc5a985459d144a13c363..a3f4374ccbce324214b4c437429b3910ef1e6936 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -1,11 +1,11 @@
 package leon
+package verification
 
 import purescala.Common._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 import purescala.Definitions._
-import Extensions.Tactic
 
 import scala.collection.mutable.{Map => MutableMap}
 
diff --git a/src/main/scala/leon/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
similarity index 99%
rename from src/main/scala/leon/InductionTactic.scala
rename to src/main/scala/leon/verification/InductionTactic.scala
index 4adc158b323678d423ce9c7bb80705ac2512fc25..360f41493440cba920be3a4f21289f33ff3e9f1b 100644
--- a/src/main/scala/leon/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -1,4 +1,5 @@
 package leon
+package verification
 
 import purescala.Common._
 import purescala.Trees._
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d19752949f393e5bad32f2824b723ea6dfabed91
--- /dev/null
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -0,0 +1,15 @@
+package leon
+package verification
+
+import Extensions.Extension
+
+import purescala.Definitions._
+
+abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
+  def setProgram(program: Program) : Unit = {}
+  def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
+  def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
+  def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
+  def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
+  def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
+}
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
similarity index 91%
rename from src/main/scala/leon/VerificationCondition.scala
rename to src/main/scala/leon/verification/VerificationCondition.scala
index e5556f1acf52fa3f8472556bcc66d3572c032488..ac972d50cbf1d3754900db64c38741b572be2324 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -1,9 +1,10 @@
-package leon
+package leon.verification
 
-import purescala.Trees._
-import purescala.Definitions._
-import purescala.Common._
-import Extensions._
+import leon.purescala.Trees._
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+
+import leon.solvers.Solver
 
 /** This is just to hold some history information. */
 class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends ScalacPositional {
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 1682054408d45c00a7721bd9a113f61fad4706d9..6b015b9afc8fac4a8fbe51828680920b555a2a40 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -8,7 +8,7 @@ import leon.purescala.TypeTrees._
 
 import leon.SilentReporter
 
-import leon.Extensions.Solver
+import leon.solvers.Solver
 import leon.solvers.z3.UninterpretedZ3Solver
 
 import org.scalatest.FunSuite