diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
deleted file mode 100644
index acc1707eb8e8762c3ef5ad0ca1a3953a8dc4de0b..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/Extensions.scala
+++ /dev/null
@@ -1,86 +0,0 @@
-package leon
-
-import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Definitions._
-
-object Extensions {
-  import leon.verification.{Analyser,Tactic}
-  import leon.solvers.Solver
-
-  abstract class Extension(reporter: Reporter) {
-    def description: String
-    def shortDescription: String = description
-  }
-
-  // The rest of the code is for dynamically loading extensions
-
-  private var allLoaded : Seq[Extension] = Nil
-  private var analysisExtensions : Seq[Analyser] = Nil
-  private var solverExtensions : Seq[Solver] = Nil
-
-  // Returns the list of the newly loaded.
-  def loadAll(extensionsReporter : Reporter = Settings.reporter) : Seq[Extension] = {
-    val allNames: Seq[String] = Settings.extensionNames
-    val loaded = (if(!allNames.isEmpty) {
-      val classLoader = Extensions.getClass.getClassLoader
-
-      val classes: Seq[Class[_]] = (for(name <- allNames) yield {
-        try {
-          classLoader.loadClass(name)
-        } catch {
-          case _ => {
-            Settings.reporter.error("Couldn't load extension class " + name) 
-            null
-          }
-        }
-      }).filter(_ != null)
-
-      classes.map(cl => {
-        try {
-          val cons = cl.getConstructor(classOf[Reporter])
-          cons.newInstance(extensionsReporter).asInstanceOf[Extension]
-        } catch {
-          case _ => {
-            Settings.reporter.error("Extension class " + cl.getName + " does not seem to be of a proper type.")
-            null
-          }
-        }
-      }).filter(_ != null)
-    } else {
-      Nil
-    })
-    if(!loaded.isEmpty) {
-      Settings.reporter.info("The following extensions are loaded:\n" + loaded.toList.map(_.description).mkString("  ", "\n  ", ""))
-    }
-    // these extensions are always loaded, unless specified otherwise
-    val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
-      val z3 : Solver = new solvers.z3.FairZ3Solver(extensionsReporter)
-      z3 :: Nil
-    } else {
-      Nil
-    }
-
-    allLoaded = defaultExtensions ++ loaded
-    analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
-    //analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
-
-    val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
-    val solverExtensions1 = if(Settings.useQuickCheck) new solvers.RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
-    val solverExtensions2 = if(Settings.useParallel) Seq(new solvers.ParallelSolver(solverExtensions1: _*)) else solverExtensions1
-    val solverExtensions3 = 
-      if(Settings.solverTimeout == None) {
-        solverExtensions2 
-      } else {
-        val t = Settings.solverTimeout.get 
-        solverExtensions2.map(s => new solvers.TimeoutSolver(s, t))
-      }
-    solverExtensions = solverExtensions3
-    loaded
-  }
-
-  def loadedExtensions : Seq[Extension] = allLoaded
-  def loadedAnalysisExtensions : Seq[Analyser] = analysisExtensions
-  def loadedSolverExtensions : Seq[Solver] = solverExtensions
-}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index f643c3a241957a7f76501f12b18974562b4f3ff6..5e2585eb5612e34cb0af33c9daa4b75c43dc4d0c 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -18,7 +18,7 @@ object Settings {
   var useCores : Boolean = false
   var pruneBranches : Boolean = false
   var solverTimeout : Option[Int] = None
-  //var luckyTest : Boolean = true
+  var luckyTest : Boolean = true
   var verifyModel : Boolean = true
   var useQuickCheck : Boolean = false
   var useParallel : Boolean = false
diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
index 3db02146e338b8b6f72c886df9072c5d98f01311..080e7d03862507899d97d9e288e04041a304ec89 100644
--- a/src/main/scala/leon/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -1,6 +1,5 @@
 package leon.isabelle
 
-import leon.Extensions._
 import leon.Reporter
 import leon.Settings._
 
@@ -20,7 +19,8 @@ import scala.collection.mutable.ListMap
 
 class Main(reporter: Reporter) extends Analyser(reporter) {
   val description = "Generates Isabelle source"
-  override val shortDescription = "isabelle"
+  val shortDescription = "isabelle"
+
   var mapParentTypes = new ListMap[String, String]
 
   //map for each function keeps the functions that it calls inside it 
diff --git a/src/main/scala/leon/isabelle/StrongConnectedComponents.scala b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
index 78eb355ff9f64f42213adaa43028eb2e999bdedb..497e16884d699b1aa1167d8c522e0182e955582d 100644
--- a/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
+++ b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
@@ -1,6 +1,5 @@
 package leon.isabelle
 
-import leon.Extensions._
 import leon.Reporter
 import leon.Settings._
 
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index 9a9e39829b3ede800d94cc7114f8c8f37224da43..6ac173414f6b483c83cd0372e3b1d02f1ecf5c8f 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -5,7 +5,6 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
-import Extensions._
 
 import Evaluator._
 
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index 89c0c6752a99c7a19f07d97b4603620a71d42bf9..3b44cae39cc712763670dd332b97e453d26a085d 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -6,7 +6,6 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.TypeTrees._
-import Extensions._
 
 import Evaluator._
 
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 947f4ce28b3d6e93a73ecec6875decddf7658a97..b31a083be787ac6d663b839e228b3bda300d709d 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -1,14 +1,16 @@
 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) {
+abstract class Solver(val reporter: Reporter) {
+  // This used to be in Extension
+  val description : String
+  val shortDescription : String
+
   // 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.) 
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 6b08a36f769188eed34030950b34fe8daec4d3be..6fa76d0bf9328f983ec2fd6de4fd27bbed6b5e6d 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -5,7 +5,6 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
-import Extensions._
 
 import scala.sys.error
 
diff --git a/src/main/scala/leon/solvers/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index 054ae3f938a9c50624a75359365c8f95ea03b2ce..b75c157d84d013ea57b4b6d39dadebc2997d49b1 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -5,7 +5,6 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
-import Extensions._
 
 class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
   val description = "Solver for syntactically trivial formulas"
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 414e8e1a4941f51659215e545b68095cdf1e30bc..20992d2e342348a76bf8324a55d8f09f2daf8546 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -7,7 +7,6 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.TypeTrees._
-import Extensions._
 
 import scala.collection.mutable.{Map => MutableMap}
 import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3659bb6685930a26c71e4e53d28a6fda5abed0ae..20341ff939c00c785024c249c92cd07c3c7ae3e7 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -11,7 +11,6 @@ import purescala.Trees._
 import purescala.Extractors._
 import purescala.TreeOps._
 import purescala.TypeTrees._
-import Extensions._
 
 import scala.collection.mutable.{Map => MutableMap}
 import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 2e2a7cf6f8bb02e4fe6bc966da4d92c31590f91b..74aef6fcda4d54622fb1ccbf0412b8cee8e3d7d8 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -11,7 +11,6 @@ import purescala.Trees._
 import purescala.Extractors._
 import purescala.TreeOps._
 import purescala.TypeTrees._
-import Extensions._
 
 /** This is a rather direct mapping to Z3, where all functions are left uninterpreted.
  *  It reports the results as follows (based on the negation of the formula):
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 5fc00acd04d18b444ad79d707f5a28145e824642..2e65ca7e56f46edb99b4ea91c4b09826c7bd2286 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -7,7 +7,6 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.TypeTrees._
-import Extensions._
 
 trait Z3ModelReconstruction {
   self: AbstractZ3Solver =>
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 3b76352b2cb457e03fb628d8318684b4e617b664..0502be54025994358d0141f98d908df134befb25 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -8,7 +8,6 @@ import leon.purescala.Trees._
 import leon.purescala.TreeOps._
 import leon.purescala.TypeTrees._
 import leon.purescala.ScalaPrinter
-import leon.Extensions._
 import leon.solvers.z3.FairZ3Solver
 import leon.Reporter
 
@@ -17,7 +16,7 @@ import scala.collection.mutable.{Set => MutableSet}
 class TestGeneration(reporter: Reporter) extends Analyser(reporter) {
 
   def description: String = "Generate random testcases"
-  override def shortDescription: String = "test"
+  def shortDescription: String = "test"
 
   private val z3Solver = new FairZ3Solver(reporter)
 
diff --git a/src/main/scala/leon/verification/Analyser.scala b/src/main/scala/leon/verification/Analyser.scala
index 84a2d87221bdfeb1d225ec6bb3542c2a5db7f4e4..708a3a7564f3366fbc8ce6849f891b91e5abee3f 100644
--- a/src/main/scala/leon/verification/Analyser.scala
+++ b/src/main/scala/leon/verification/Analyser.scala
@@ -1,12 +1,10 @@
 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) {
+abstract class Analyser(reporter: 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/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
index 1521ad8e1e3fa4ad42d36664d76d27a5fed4966c..77cebb21160c472b0d64f0d7ec3fb90b5943e47d 100644
--- a/src/main/scala/leon/verification/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -7,22 +7,20 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.TypeTrees._
 
-import Extensions._
-
 import solvers.{Solver,TrivialSolver}
+import solvers.z3.FairZ3Solver
 
 import scala.collection.mutable.{Set => MutableSet}
 
 class Analysis(val program : Program, val reporter: Reporter) {
-  Extensions.loadAll(reporter)
 
-  val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
+  val trivialSolver = new TrivialSolver(reporter)
 
-  val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
+  val fairZ3 = new FairZ3Solver(reporter)
 
-  val solverExtensions: Seq[Solver] = trivialSolver +: loadedSolverExtensions
+  val solvers : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
 
-  solverExtensions.foreach(_.setProgram(program))
+  solvers.foreach(_.setProgram(program))
 
   val defaultTactic = new DefaultTactic(reporter)
   defaultTactic.setProgram(program)
@@ -40,7 +38,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
       FunctionTemplate.mkTemplate(funDef)
     }
 
-    val report = if(solverExtensions.size > 1) {
+    val report = if(solvers.size > 1) {
       reporter.info("Running verification condition generation...")
       checkVerificationConditions(generateVerificationConditions)
     } else {
@@ -48,10 +46,11 @@ class Analysis(val program : Program, val reporter: Reporter) {
       VerificationReport.emptyReport
     }
 
-    analysisExtensions.foreach(ae => {
-      reporter.info("Running analysis from extension: " + ae.description)
-      ae.analyse(program)
-    })
+    // This used to be for additional analyses. They should now just be different phases.
+    // analysisExtensions.foreach(ae => {
+    //   reporter.info("Running analysis from extension: " + ae.description)
+    //   ae.analyse(program)
+    // })
 
     report
   }
@@ -105,7 +104,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
 
       // try all solvers until one returns a meaningful answer
       var superseeded : Set[String] = Set.empty[String]
-      solverExtensions.find(se => {
+      solvers.find(se => {
         reporter.info("Trying with solver: " + se.shortDescription)
         if(superseeded(se.shortDescription) || superseeded(se.description)) {
           reporter.info("Solver was superseeded. Skipping.")
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index d19752949f393e5bad32f2824b723ea6dfabed91..3a00f2ab7f9a7dfcd731b0e48273af09de60f544 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -1,11 +1,12 @@
 package leon
 package verification
 
-import Extensions.Extension
-
 import purescala.Definitions._
 
-abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
+abstract class Tactic(reporter: Reporter) {
+  val description : String
+  val shortDescription : String
+
   def setProgram(program: Program) : Unit = {}
   def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
   def generatePreconditions(function: FunDef) : Seq[VerificationCondition]