diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 8be9ae0b38b9eff8334117bcfc04714247311e7d..f0eee53a67cbe379212745dc71c159f421bcb9e8 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -2,6 +2,8 @@
 
 package leon
 
+import leon.utils._
+
 import purescala.Definitions.Program
 import java.io.File
 
@@ -9,8 +11,9 @@ import java.io.File
  *  Contexts are immutable, and so should all there fields (with the possible
  *  exception of the reporter). */
 case class LeonContext(
+  reporter: Reporter,
+  interruptManager: InterruptManager,
   settings: Settings = Settings(),
   options: Seq[LeonOption] = Seq(),
-  files: Seq[File] = Seq(),
-  reporter: Reporter = new DefaultReporter()
+  files: Seq[File] = Seq()
 )
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 6bec43bb378eec44a61dc7eb04f60f7b98c1deae..b3b2736f1888b0d311fd959d15bf47700b094755 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -2,6 +2,8 @@
 
 package leon
 
+import leon.utils._
+
 object Main {
 
   lazy val allPhases: List[LeonPhase[_, _]] = {
@@ -58,7 +60,7 @@ object Main {
   def processOptions(args: Seq[String]): LeonContext = {
     val phases = allPhases
 
-    val initReporter = new DefaultReporter()
+    val initReporter = new DefaultReporter(Settings())
 
     val allOptions = this.allOptions
 
@@ -155,8 +157,8 @@ object Main {
       case _ =>
     }
 
-    // Create a new reporter taking debugSections into account
-    val reporter = new DefaultReporter(settings.debugSections)
+    // Create a new reporter taking settings into account
+    val reporter = new DefaultReporter(settings)
 
     reporter.ifDebug(ReportingOptions) {
       val debug = reporter.debug(ReportingOptions)_
@@ -171,7 +173,15 @@ object Main {
       }
     }
 
-    LeonContext(settings = settings, reporter = reporter, files = files, options = leonOptions)
+    val intManager = new InterruptManager(reporter)
+
+    intManager.registerSignalHandler()
+
+    LeonContext(settings = settings,
+                reporter = reporter,
+                files = files,
+                options = leonOptions,
+                interruptManager = intManager)
   }
 
   def computePipeline(settings: Settings): Pipeline[List[String], Any] = {
@@ -197,8 +207,6 @@ object Main {
   }
 
   def main(args : Array[String]) {
-    val reporter = new DefaultReporter()
-
     // Process options
     val ctx = processOptions(args.toList)
 
@@ -209,10 +217,10 @@ object Main {
       // Run pipeline
       pipeline.run(ctx)(args.toList) match {
         case report: verification.VerificationReport =>
-          reporter.info(report.summaryString)
+          ctx.reporter.info(report.summaryString)
 
         case report: termination.TerminationReport =>
-          reporter.info(report.summaryString)
+          ctx.reporter.info(report.summaryString)
 
         case _ =>
       }
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 02840858374505ebf50a4089d6aa7d4189e0583e..63478b4b7113836c08196b61c393241b5d5f478c 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -6,12 +6,12 @@ import purescala.Definitions.Definition
 import purescala.Trees.Expr
 import purescala.PrettyPrinter
 
-abstract class Reporter(enabledSections: Set[ReportingSection]) {
+abstract class Reporter(settings: Settings) {
   def infoFunction(msg: Any) : Unit
   def warningFunction(msg: Any) : Unit
   def errorFunction(msg: Any) : Unit
-  def fatalErrorFunction(msg: Any) : Nothing
   def debugFunction(msg: Any) : Unit
+  def fatalErrorFunction(msg: Any) : Nothing
 
   // This part of the implementation is non-negociable.
   private var _errorCount : Int = 0
@@ -34,21 +34,22 @@ abstract class Reporter(enabledSections: Set[ReportingSection]) {
     fatalErrorFunction(msg)
   }
 
-  val debugMask = enabledSections.foldLeft(0){ _ | _.mask }
+  private val debugMask = settings.debugSections.foldLeft(0){ _ | _.mask }
 
-  final def debug(section: ReportingSection)(msg: => Any) = {
-    ifDebug(section) { debugFunction(msg) }
-  }
-
-  final def ifDebug(section: ReportingSection)(body: => Unit) = {
+  def ifDebug(section: ReportingSection)(body: => Any) {
     if ((debugMask & section.mask) == section.mask) {
       body
     }
   }
-}
 
+  def debug(section: ReportingSection)(msg: => Any) {
+    ifDebug(section) {
+      debugFunction(msg)
+    }
+  }
+}
 
-class DefaultReporter(enabledSections: Set[ReportingSection] = Set()) extends Reporter(enabledSections) {
+class DefaultReporter(settings: Settings) extends Reporter(settings) {
   protected val errorPfx   = "[ Error ] "
   protected val warningPfx = "[Warning] "
   protected val infoPfx    = "[ Info  ] "
@@ -71,11 +72,14 @@ class DefaultReporter(enabledSections: Set[ReportingSection] = Set()) extends Re
     msg.replaceAll("\n", "\n" + (" " * (pfx.size)))
   }
 
-  def errorFunction(msg: Any) = output(reline(errorPfx, msg.toString))
+  def errorFunction(msg: Any)   = output(reline(errorPfx, msg.toString))
   def warningFunction(msg: Any) = output(reline(warningPfx, msg.toString))
-  def infoFunction(msg: Any) = output(reline(infoPfx, msg.toString))
-  def fatalErrorFunction(msg: Any) = { output(reline(fatalPfx, msg.toString)); throw LeonFatalError() }
-  def debugFunction(msg: Any) = output(reline(debugPfx, msg.toString))
+  def infoFunction(msg: Any)    = output(reline(infoPfx, msg.toString))
+  def debugFunction(msg: Any)   = output(reline(debugPfx, msg.toString))
+  def fatalErrorFunction(msg: Any) = {
+    output(reline(fatalPfx, msg.toString));
+    throw LeonFatalError()
+  }
 }
 
 sealed abstract class ReportingSection(val name: String, val mask: Int)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index f55c4956712b9ffbf976aefdc47378c90d41595e..0003f17cff07c284af3b7d52d8d6ab2530c288b5 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -3,6 +3,8 @@
 package leon
 package solvers.z3
 
+import leon.utils._
+
 import z3.scala._
 import purescala.Common._
 import purescala.Definitions._
@@ -16,12 +18,17 @@ 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 extends solvers.IncrementalSolverBuilder {
+trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder with Interruptible {
   self: leon.solvers.Solver =>
 
   val context : LeonContext
   protected[z3] val reporter : Reporter = context.reporter
 
+  context.interruptManager.registerForInterrupts(this)
+  def interrupt() {
+    halt()
+  }
+
   class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
 
   protected[leon] val z3cfg : Z3Config
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 78d2e1d2b273c2b0b429e48fdab69857b7d35fa8..2930067d03de8a9bebda6c1761735ee2fd9da992 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -3,6 +3,8 @@
 package leon
 package solvers.z3
 
+import leon.utils._
+
 import z3.scala._
 
 import leon.solvers.Solver
@@ -29,7 +31,7 @@ class FairZ3Solver(context : LeonContext)
 
   enclosing =>
 
-  def debug(s: String) = context.reporter.debug(ReportingSolver)(s)
+  val debug = context.reporter.debug(ReportingSolver)_
 
   // What wouldn't we do to avoid defining vars?
   val (feelingLucky, checkModels, useCodeGen, evalGroundApps, unrollUnsatCores) = locally {
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 713fcdd0b72177d5aef97e6f1873cf2ae67b172a..65cb7be3bd4840a7664a1026d7a18ef5619c3a71 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -8,18 +8,14 @@ import purescala.Trees._
 import purescala.TreeNormalizations.linearArithmeticForm
 import purescala.TypeTrees._
 import purescala.Common._
+import evaluators._
 
 import synthesis.Algebra._
 
 object LinearEquations {
-  // This is a hack, but the use of an evaluator in this file is itself beyond that.
-  import evaluators._
-  // TODO: Kill with fire
-  private lazy val evaluator = new DefaultEvaluator(LeonContext(Settings(), Seq(), Seq(), new DefaultReporter()), Program.empty)
-
   //eliminate one variable from normalizedEquation t + a1*x1 + ... + an*xn = 0
   //return a mapping for each of the n variables in (pre, map, freshVars)
-  def elimVariable(as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr], List[Identifier]) = {
+  def elimVariable(evaluator: Evaluator, as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr], List[Identifier]) = {
     require(normalizedEquation.size > 1)
     require(normalizedEquation.tail.forall{case IntLiteral(i) if i != 0 => true case _ => false})
     val t: Expr = normalizedEquation.head
@@ -35,9 +31,9 @@ object LinearEquations {
     } else if(d > 1) {
       val newCoefsParams: List[Expr] = coefsParams.map(i => IntLiteral(i/d) : Expr)
       val newT = newCoefsParams.zip(IntLiteral(1)::orderedParams.map(Variable(_)).toList).foldLeft[Expr](IntLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
-      elimVariable(as, newT :: normalizedEquation.tail.map{case IntLiteral(i) => IntLiteral(i/d) : Expr})
+      elimVariable(evaluator, as, newT :: normalizedEquation.tail.map{case IntLiteral(i) => IntLiteral(i/d) : Expr})
     } else {
-      val basis: Array[Array[Int]]  = linearSet(as, normalizedEquation.tail.map{case IntLiteral(i) => i}.toArray)
+      val basis: Array[Array[Int]]  = linearSet(evaluator, as, normalizedEquation.tail.map{case IntLiteral(i) => i}.toArray)
       val (pre, sol) = particularSolution(as, normalizedEquation)
       val freshVars: Array[Identifier] = basis(0).map(_ => FreshIdentifier("v", true).setType(Int32Type))
 
@@ -62,7 +58,7 @@ object LinearEquations {
   //Intuitively, we are building a "basis" for the "vector space" of solutions (although we are over
   //integers, so it is not a vector space).
   //we are returning a matrix where the columns are the vectors
-  def linearSet(as: Set[Identifier], coef: Array[Int]): Array[Array[Int]] = {
+  def linearSet(evaluator: Evaluator, as: Set[Identifier], coef: Array[Int]): Array[Array[Int]] = {
 
     val K = Array.ofDim[Int](coef.size, coef.size-1)
     for(i <- 0 until K.size) {
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index ae02170fd95dc33dcc6ecc0a27b6e1313cf970cb..78e30e87facdd56c0fe26c2c23f428e74afe5cb7 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -41,14 +41,6 @@ class ParallelSearch(synth: Synthesizer,
     ctx
   }
 
-  override def stop() = {
-    synth.shouldStop.set(true)
-    for (ctx <- contexts) {
-      ctx.solver.halt()
-    }
-    super.stop()
-  }
-
   def expandAndTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskRunRule) = {
     val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
 
diff --git a/src/main/scala/leon/synthesis/SearchCostModel.scala b/src/main/scala/leon/synthesis/SearchCostModel.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b183ebabf3cf50a086775782e0de7a9b466a9b50
--- /dev/null
+++ b/src/main/scala/leon/synthesis/SearchCostModel.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
+package leon
+package synthesis
+
+import synthesis.search._
+
+case class SearchCostModel(cm: CostModel) extends AOCostModel[TaskRunRule, TaskTryRules, Solution] {
+  def taskCost(t: AOTask[Solution]) = t match {
+    case ttr: TaskRunRule =>
+      cm.ruleAppCost(ttr.app)
+    case trr: TaskTryRules =>
+      cm.problemCost(trr.p)
+  }
+
+  def solutionCost(s: Solution) = cm.solutionCost(s)
+}
+
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 9c47c9e38ab4eb479e9349551ec555010cca035d..0a0f96d27756cea51aac2fdfd52106b2c0990c44 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -3,41 +3,14 @@
 package leon
 package synthesis
 
+import leon.utils._
 import purescala.Definitions.FunDef
-
 import synthesis.search._
 
-case class TaskRunRule(app: RuleInstantiation) extends AOAndTask[Solution] {
-
-  val problem = app.problem
-  val rule    = app.rule
-
-  def composeSolution(sols: List[Solution]): Option[Solution] = {
-    app.onSuccess(sols)
-  }
-
-  override def toString = rule.name
-}
-
-case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
-  override def toString = p.toString
-}
-
-case class SearchCostModel(cm: CostModel) extends AOCostModel[TaskRunRule, TaskTryRules, Solution] {
-  def taskCost(t: AOTask[Solution]) = t match {
-    case ttr: TaskRunRule =>
-      cm.ruleAppCost(ttr.app)
-    case trr: TaskTryRules =>
-      cm.problemCost(trr.p)
-  }
-
-  def solutionCost(s: Solution) = cm.solutionCost(s)
-}
-
 class SimpleSearch(synth: Synthesizer,
                    problem: Problem,
                    rules: Seq[Rule],
-                   costModel: CostModel) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel))) {
+                   costModel: CostModel) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel))) with Interruptible {
 
   def this(synth: Synthesizer, problem: Problem) = {
     this(synth, problem, synth.rules, synth.options.costModel)
@@ -186,7 +159,6 @@ class SimpleSearch(synth: Synthesizer,
   }
 
 
-  var shouldStop = false
 
   def searchStep() {
     nextLeaf() match {
@@ -204,6 +176,19 @@ class SimpleSearch(synth: Synthesizer,
     }
   }
 
+  sctx.context.interruptManager.registerForInterrupts(this)
+
+  def interrupt() {
+    stop()
+  }
+
+  private var shouldStop = false
+
+  override def stop() {
+    super.stop()
+    shouldStop = true
+  }
+
   def search(): Option[(Solution, Boolean)] = {
     sctx.solver.init()
 
@@ -214,10 +199,4 @@ class SimpleSearch(synth: Synthesizer,
     }
     g.tree.solution.map(s => (s, g.tree.isTrustworthy))
   }
-
-  override def stop() {
-    super.stop()
-    shouldStop = true
-    sctx.solver.halt()
-  }
 }
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index d12a05c5c99c09b92961bd774b499d1d5f818a2b..7c1c29b1ba11130d4dda6a0bf3ee111f3e2a92b6 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -17,8 +17,7 @@ case class SynthesisContext(
   program: Program,
   solver: Solver,
   simpleSolver: Solver,
-  reporter: Reporter,
-  shouldStop: AtomicBoolean
+  reporter: Reporter
 )
 
 object SynthesisContext {
@@ -30,8 +29,7 @@ object SynthesisContext {
       synth.program,
       synth.solver,
       synth.simpleSolver,
-      synth.reporter,
-      synth.shouldStop)
+      synth.reporter)
   }
 }
 
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index a0d1e19a79d89d46270638e4076cddf7b9cd0a10..e77cf00694131b61ba0733b1b813c7c4189a1109 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -10,7 +10,6 @@ import purescala.Trees._
 import purescala.ScalaPrinter
 import solvers.z3._
 import solvers.TimeoutSolver
-import sun.misc.{Signal, SignalHandler}
 
 import solvers.Solver
 import java.io.File
@@ -19,8 +18,6 @@ import collection.mutable.PriorityQueue
 
 import synthesis.search._
 
-import java.util.concurrent.atomic.AtomicBoolean
-
 class Synthesizer(val context : LeonContext,
                   val functionContext: Option[FunDef],
                   val program: Program,
@@ -37,8 +34,6 @@ class Synthesizer(val context : LeonContext,
 
   val reporter = context.reporter
 
-  var shouldStop = new AtomicBoolean(false)
-
   def synthesize(): (Solution, Boolean) = {
 
     val search = if (options.manualSearch) {
@@ -55,20 +50,6 @@ class Synthesizer(val context : LeonContext,
         }
       }
 
-    val sigINT = new Signal("INT")
-    var oldHandler: SignalHandler = null
-    oldHandler = Signal.handle(sigINT, new SignalHandler {
-      def handle(sig: Signal) {
-        println
-        reporter.info("Aborting...")
-
-        shouldStop.set(true)
-        search.stop()
-
-        Signal.handle(sigINT, oldHandler)
-      }
-    })
-
     val ts = System.currentTimeMillis()
 
     val res = search.search()
diff --git a/src/main/scala/leon/synthesis/TaskRunRule.scala b/src/main/scala/leon/synthesis/TaskRunRule.scala
new file mode 100644
index 0000000000000000000000000000000000000000..642820672d4a0cd4716ac8f131e7ecd0786cbe6c
--- /dev/null
+++ b/src/main/scala/leon/synthesis/TaskRunRule.scala
@@ -0,0 +1,16 @@
+package leon
+package synthesis
+
+import synthesis.search._
+
+case class TaskRunRule(app: RuleInstantiation) extends AOAndTask[Solution] {
+
+  val problem = app.problem
+  val rule    = app.rule
+
+  def composeSolution(sols: List[Solution]): Option[Solution] = {
+    app.onSuccess(sols)
+  }
+
+  override def toString = rule.name
+}
diff --git a/src/main/scala/leon/synthesis/TaskTryRules.scala b/src/main/scala/leon/synthesis/TaskTryRules.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4ede43ce0bcfa266b590966aae4d78e9d4db4eaa
--- /dev/null
+++ b/src/main/scala/leon/synthesis/TaskTryRules.scala
@@ -0,0 +1,8 @@
+package leon
+package synthesis
+
+import synthesis.search._
+
+case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
+  override def toString = p.toString
+}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 0905e41735a63fe217833c019779f39f3c1eff71..e5a459fc6f6c68ae70f4a8db6bcea043c5a8d4c6 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -38,6 +38,8 @@ case object CEGIS extends Rule("CEGIS") {
     val filterThreshold       = 1.0/2
     val evaluator             = new CodeGenEvaluator(sctx.context, sctx.program)
 
+    val interruptManager      = sctx.context.interruptManager
+
     case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
 
     var generators = Map[TypeTree, Generator]()
@@ -624,7 +626,7 @@ case object CEGIS extends Rule("CEGIS") {
 
             val bss = ndProgram.bss
 
-            while (result.isEmpty && !needMoreUnrolling && !sctx.shouldStop.get) {
+            while (result.isEmpty && !needMoreUnrolling && !interruptManager.isInterrupted()) {
 
               solver1.checkAssumptions(bssAssumptions.map(id => Not(Variable(id)))) match {
                 case Some(true) =>
@@ -761,7 +763,7 @@ case object CEGIS extends Rule("CEGIS") {
             }
 
             unrolings += 1
-          } while(unrolings < maxUnrolings && result.isEmpty && !sctx.shouldStop.get)
+          } while(unrolings < maxUnrolings && result.isEmpty && !interruptManager.isInterrupted())
 
           result.getOrElse(RuleApplicationImpossible)
 
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 06a2398fd180f466722cd35b129677c42e2ec844..efbc68ef0f3b1537976d2819ead2fb3f4455b1e6 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -12,6 +12,7 @@ import purescala.TreeNormalizations._
 import purescala.TypeTrees._
 import purescala.Definitions._
 import LinearEquations.elimVariable
+import evaluators._
 
 case object IntegerEquation extends Rule("Integer Equation") {
   def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = if(!problem.xs.exists(_.getType == Int32Type)) Nil else {
@@ -22,6 +23,8 @@ case object IntegerEquation extends Rule("Integer Equation") {
     var candidates: Seq[Expr] = eqs
     var allOthers: Seq[Expr] = others
 
+    val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
+
     var vars: Set[Identifier] = Set()
     var eqxs: List[Identifier] = List()
 
@@ -65,7 +68,7 @@ case object IntegerEquation extends Rule("Integer Equation") {
           List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
 
         } else {
-          val (eqPre0, eqWitness, freshxs) = elimVariable(eqas, normalizedEq)
+          val (eqPre0, eqWitness, freshxs) = elimVariable(evaluator, eqas, normalizedEq)
           val eqPre = eqPre0 match {
             case Equals(Modulo(_, IntLiteral(1)), _) => BooleanLiteral(true)
             case c => c
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 6350e19b2651c31a42d70af62fb748c9e0e9a088..24023d0eafae3c2629ca3d85c4f25464fb59ae6e 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -3,6 +3,7 @@
 package leon.synthesis.utils
 
 import leon._
+import leon.utils._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
 import leon.purescala.TreeOps._
@@ -73,7 +74,6 @@ object Benchmarks extends App {
   var nSuccessTotal, nInnapTotal, nDecompTotal, nAltTotal = 0
   var tTotal: Long = 0
 
-  val reporter = new DefaultReporter()
   val ctx = leon.Main.processOptions(others ++ newOptions)
 
   for (file <- ctx.files) {
@@ -99,8 +99,7 @@ object Benchmarks extends App {
         program         = program,
         solver          = solver,
         simpleSolver    = simpleSolver,
-        reporter        = reporter,
-        shouldStop      = new java.util.concurrent.atomic.AtomicBoolean
+        reporter        = ctx.reporter
       )
 
       val ts = System.currentTimeMillis
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
new file mode 100644
index 0000000000000000000000000000000000000000..23f2221ee61d06382251ff854e5165b23ac341d3
--- /dev/null
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -0,0 +1,46 @@
+package leon
+package utils
+
+import scala.collection.JavaConversions._
+
+import java.util.concurrent.atomic.AtomicBoolean
+import sun.misc.{Signal, SignalHandler}
+import java.util.WeakHashMap
+
+class InterruptManager(reporter: Reporter) {
+  private[this] val interruptibles = new WeakHashMap[Interruptible, Boolean]()
+  private[this] val sigINT = new Signal("INT")
+  private[this] var oldHandler: SignalHandler = null
+
+  val interrupted: AtomicBoolean = new AtomicBoolean(false)
+
+  @inline
+  def isInterrupted() = interrupted.get()
+
+  def interrupt() = synchronized {
+    if (!interrupted.get()) {
+      interrupted.set(true)
+
+      interruptibles.keySet.foreach(_.interrupt())
+    } else {
+      reporter.warning("Already interrupted!")
+    }
+  }
+
+  def registerForInterrupts(i: Interruptible) {
+    interruptibles.put(i, true)
+  }
+
+  def registerSignalHandler() {
+    oldHandler = Signal.handle(sigINT, new SignalHandler {
+      def handle(sig: Signal) {
+        println
+        reporter.info("Aborting...")
+
+        interrupt()
+
+        Signal.handle(sigINT, oldHandler)
+      }
+    })
+  }
+}
diff --git a/src/main/scala/leon/utils/Interruptible.scala b/src/main/scala/leon/utils/Interruptible.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1fe7b73903a3f582cb9906f14c6d608fd2a57e82
--- /dev/null
+++ b/src/main/scala/leon/utils/Interruptible.scala
@@ -0,0 +1,6 @@
+package leon
+package utils
+
+trait Interruptible {
+  def interrupt(): Unit
+}
diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/utils/Stopwatch.scala
similarity index 98%
rename from src/main/scala/leon/Stopwatch.scala
rename to src/main/scala/leon/utils/Stopwatch.scala
index 9eab173d92751c8618cdc5d9b4149dc94a0c0ef4..38b38bbf35cfe7510a4b94d179ebcbc6dea63c53 100644
--- a/src/main/scala/leon/Stopwatch.scala
+++ b/src/main/scala/leon/utils/Stopwatch.scala
@@ -1,6 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 package leon
+package utils
 
 class StopwatchCollection(name: String) {
   var acc: Long = 0L
diff --git a/src/main/scala/leon/SubtypingPhase.scala b/src/main/scala/leon/utils/SubtypingPhase.scala
similarity index 99%
rename from src/main/scala/leon/SubtypingPhase.scala
rename to src/main/scala/leon/utils/SubtypingPhase.scala
index 350c7ddac18d333505d2654275a98f962720e318..37230604196a655cf68acdbe23eb6066e4bfcd6f 100644
--- a/src/main/scala/leon/SubtypingPhase.scala
+++ b/src/main/scala/leon/utils/SubtypingPhase.scala
@@ -1,6 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 package leon
+package utils
 
 import purescala.Common._
 import purescala.TypeTrees._
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
similarity index 99%
rename from src/main/scala/leon/UnitElimination.scala
rename to src/main/scala/leon/utils/UnitElimination.scala
index 3717cd585cb76c7048f40e733bfe6672ad3511c4..c6e9cf4abb3e0a588b09c115e8e323c35db54ac1 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -1,6 +1,7 @@
 /* Copyright 2009-2013 EPFL, Lausanne */
 
 package leon
+package utils
 
 import purescala.Common._
 import purescala.Definitions._
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 193ebcb75fb4d917c910e9d0ed5745999b7559c8..1113daca80e27eec4054900e75ed49ce3e50dae6 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -61,7 +61,9 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
     val reporter = vctx.reporter
     val solvers  = vctx.solvers
 
-    for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1 < b._1); vcInfo <- vcs if !vctx.shouldStop.get()) {
+    val interruptManager = vctx.context.interruptManager
+
+    for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1 < b._1); vcInfo <- vcs if !interruptManager.isInterrupted()) {
       val funDef = vcInfo.funDef
       val vc = vcInfo.condition
 
@@ -88,7 +90,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
           val dt = ((t2 - t1) / 1000000) / 1000.0
 
           solverResult match {
-            case _ if vctx.shouldStop.get() =>
+            case _ if interruptManager.isInterrupted() =>
               reporter.info("=== CANCELLED ===")
               vcInfo.time = Some(dt)
               false
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index aede661c0e32e23d08e1c9057856f4c72cf2c4a1..f4141f20170db79e8d00c2de8b885fb56efd9ffa 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -10,6 +10,5 @@ import java.util.concurrent.atomic.AtomicBoolean
 case class VerificationContext (
   context: LeonContext,
   solvers: Seq[Solver],
-  reporter: Reporter,
-  shouldStop: AtomicBoolean = new AtomicBoolean(false)
+  reporter: Reporter
 )
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index 3ee2480d62ab726e5fb050bddf9f1fd6ab68524c..202a76fb7545a2d207738d93172259507bb7e978 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -1,4 +1,8 @@
-package leon.test
+package leon
+package test
+
+import leon.utils._
+
 import scala.io.Source
 import org.scalatest._
 import org.scalatest.concurrent._
@@ -28,6 +32,20 @@ trait LeonTestSuite extends FunSuite with Timeouts {
     def withValue(v: Long) = this.copy(v :: values)
   }
 
+
+  var testContext = generateContext
+
+  def generateContext = {
+    val reporter = new TestSilentReporter
+
+    LeonContext(
+      settings = Settings(),
+      files = List(),
+      reporter = reporter,
+      interruptManager = new InterruptManager(reporter)
+    )
+  }
+
   def testIdentifier(name: String): String = {
     (this.getClass.getName+"-"+name).replaceAll("[^0-9a-zA-Z-]", "")
   }
@@ -69,11 +87,19 @@ trait LeonTestSuite extends FunSuite with Timeouts {
     fw.close
   }
 
+  override implicit val defaultInterruptor = new Interruptor {
+    def apply(t: Thread) {
+      testContext.interruptManager.interrupt()
+    }
+  }
+
   override def test(name: String, tags: Tag*)(body: => Unit) {
     super.test(name, tags: _*) {
       val id = testIdentifier(name)
       val ts = now()
 
+      testContext = generateContext
+
       failAfter(2.minutes) {
         body
       }
diff --git a/src/test/scala/leon/test/TestSilentReporter.scala b/src/test/scala/leon/test/TestSilentReporter.scala
index c396bded57d035101871ea1dea1283930dedade7..8cbde4ab1a6fbaba3b644002cc162ec5130f46c6 100644
--- a/src/test/scala/leon/test/TestSilentReporter.scala
+++ b/src/test/scala/leon/test/TestSilentReporter.scala
@@ -1,6 +1,6 @@
 package leon
 package test
 
-class TestSilentReporter extends DefaultReporter() {
-  override def output(msg: String) : Unit = {}
+class TestSilentReporter extends DefaultReporter(Settings()) {
+  override def output(msg: String) : Unit = { }
 }
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index edcc0c9b5f1a56ea16e0abdf4877e212b3365f30..c20a80028aca7f6509b7f889c5e6be8bc115592c 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -15,15 +15,7 @@ import leon.purescala.Trees._
 import leon.purescala.TypeTrees._
 
 class EvaluatorsTests extends LeonTestSuite {
-  private implicit lazy val leonContext = LeonContext(
-    settings = Settings(
-      synthesis = false,
-      xlang     = false,
-      verify    = false
-    ),
-    files = List(),
-    reporter = new TestSilentReporter
-  )
+  private implicit lazy val leonContext = testContext
 
   private val evaluatorConstructors : List[(LeonContext,Program)=>Evaluator] = List(
     new DefaultEvaluator(_,_),
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index 99659fb690edd55b67641d2117b120dd7b21a4e5..8f73d73900d3161f9ce7729f66514f0cc769a9a6 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -17,26 +17,16 @@ import leon.evaluators._
 import org.scalatest.FunSuite
 
 class DataGen extends LeonTestSuite {
-  private implicit lazy val leonContext = LeonContext(
-    settings = Settings(
-      synthesis = false,
-      xlang     = false,
-      verify    = false
-    ),
-    files = List(),
-    reporter = new TestSilentReporter
-  )
-
   private def parseString(str : String) : Program = {
     val pipeline = TemporaryInputPhase andThen ExtractionPhase
 
-    val errorsBefore   = leonContext.reporter.errorCount
-    val warningsBefore = leonContext.reporter.warningCount
+    val errorsBefore   = testContext.reporter.errorCount
+    val warningsBefore = testContext.reporter.warningCount
 
-    val program = pipeline.run(leonContext)((str, Nil))
+    val program = pipeline.run(testContext)((str, Nil))
   
-    assert(leonContext.reporter.errorCount   === errorsBefore)
-    assert(leonContext.reporter.warningCount === warningsBefore)
+    assert(testContext.reporter.errorCount   === errorsBefore)
+    assert(testContext.reporter.warningCount === warningsBefore)
 
     program
   }
@@ -70,8 +60,8 @@ class DataGen extends LeonTestSuite {
 
     val prog = parseString(p)
 
-    val eval      = new DefaultEvaluator(leonContext, prog)
-    val generator = new NaiveDataGen(leonContext, prog, eval)
+    val eval      = new DefaultEvaluator(testContext, prog)
+    val generator = new NaiveDataGen(testContext, prog, eval)
 
     generator.generate(BooleanType).toSet.size === 2
     generator.generate(TupleType(Seq(BooleanType,BooleanType))).toSet.size === 4
@@ -86,7 +76,7 @@ class DataGen extends LeonTestSuite {
 
     generator.generate(listType).take(100).toSet.size === 100
 
-    val evaluator = new CodeGenEvaluator(leonContext, prog)
+    val evaluator = new CodeGenEvaluator(testContext, prog)
 
     val a = Variable(FreshIdentifier("a").setType(Int32Type))
     val b = Variable(FreshIdentifier("b").setType(Int32Type))
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index 1267b794a38f6a3467136268b8a885f2a77f5938..7c85c4ae2c7fcf522934f978b4a12e69364a6e6d 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -16,8 +16,8 @@ import leon.purescala.Trees._
  * This is a probabilistic based approach, it does not rely on any external solver and can
  * only prove the non equality of two expressions.
  */
-object LikelyEq {
-  private lazy val evaluator : Evaluator = new DefaultEvaluator(LeonContext(reporter = new TestSilentReporter), Program.empty)
+object LikelyEq extends LeonTestSuite {
+  private lazy val evaluator : Evaluator = new DefaultEvaluator(testContext, Program.empty)
 
   private val min = -5
   private val max = 5
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 823383baf499e319ccdd66e5ef83c6273eee167c..6372a364acd6a33c353e5aba87587f29c98ddce8 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -12,11 +12,10 @@ import leon.purescala.TypeTrees._
 import leon.purescala.TreeOps._
 
 class TreeOpsTests extends LeonTestSuite {
-  private val silentContext = LeonContext(reporter = new TestSilentReporter)
   
   test("Path-aware simplifications") {
     import leon.solvers.z3.UninterpretedZ3Solver
-    val solver = new UninterpretedZ3Solver(silentContext)
+    val solver = new UninterpretedZ3Solver(testContext)
     solver.setProgram(Program.empty)
 
     // TODO actually testing something here would be better, sorry
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 954d30e65edb7294fa13d0d12d10a85cc5fc530e..a8f1ddd0859c03eb605c2323d7c2d4057d18f00c 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -28,7 +28,7 @@ class TimeoutSolverTests extends LeonTestSuite {
   }
 
   private def getTOSolver : Solver = {
-    val s = new TimeoutSolver(new IdioticSolver(LeonContext()), 1000L)
+    val s = new TimeoutSolver(new IdioticSolver(testContext), 1000L)
     s.setProgram(Program.empty)
     s
   }
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 68a41d0ce237d491801fe86fc59b8c75788b87eb..075522597e506554d32f21293253cff3a5877d6d 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -3,8 +3,6 @@
 package leon.test
 package solvers.z3
 
-import leon.LeonContext
-
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
@@ -39,8 +37,6 @@ class FairZ3SolverTests extends LeonTestSuite {
     "Solver should not be able to decide the formula " + expr + "."
   )
 
-  private val silentContext = LeonContext(reporter = new TestSilentReporter)
-
   // def f(fx : Int) : Int = fx + 1
   private val fx   : Identifier = FreshIdentifier("x").setType(Int32Type)
   private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
@@ -57,7 +53,7 @@ class FairZ3SolverTests extends LeonTestSuite {
   private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
   private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
 
-  private val solver = new FairZ3Solver(silentContext)
+  private val solver = new FairZ3Solver(testContext)
   solver.setProgram(minimalProgram)
 
   private val tautology1 : Expr = BooleanLiteral(true)
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 802bd13f057f873d764b234dd51e166138b198e0..385784d9ac8a49d8e0b3d047c52cda15e19fc9cc 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -3,8 +3,6 @@
 package leon.test
 package solvers.z3
 
-import leon.LeonContext
-
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
@@ -43,8 +41,6 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
     "Solver should not be able to decide the formula " + expr + "."
   )
 
-  private val silentContext = LeonContext(reporter = new TestSilentReporter)
-
   // def f(fx : Int) : Int = fx + 1
   private val fx   : Identifier = FreshIdentifier("x").setType(Int32Type)
   private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
@@ -61,7 +57,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
   private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
   private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
 
-  private val solver = new FairZ3Solver(silentContext)
+  private val solver = new FairZ3Solver(testContext)
   solver.setProgram(minimalProgram)
   solver.restartZ3
 
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 339d5bf2a0af1aebee6e4231be594cfed8cfe876..8f4cd84662316526f08650aa1fc05679b1c2ff4b 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -3,8 +3,6 @@
 package leon.test
 package solvers.z3
 
-import leon.LeonContext
-
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._
@@ -39,8 +37,6 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
     "Solver should not be able to decide the formula " + expr + "."
   )
 
-  private val silentContext = LeonContext(reporter = new TestSilentReporter)
-
   // def f(fx : Int) : Int = fx + 1
   private val fx   : Identifier = FreshIdentifier("x").setType(Int32Type)
   private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Int32Type, VarDecl(fx, Int32Type) :: Nil)
@@ -62,7 +58,7 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
   private def f(e : Expr) : Expr = FunctionInvocation(fDef, e :: Nil)
   private def g(e : Expr) : Expr = FunctionInvocation(gDef, e :: Nil)
 
-  private val solver = new UninterpretedZ3Solver(silentContext)
+  private val solver = new UninterpretedZ3Solver(testContext)
   solver.setProgram(minimalProgram)
 
   private val tautology1 : Expr = BooleanLiteral(true)
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 03b3e66a87e68ca8fd126433b10f8442d98d891f..b2d8ad775ca528ad0f596b77e6ee1429d63932b2 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -7,7 +7,10 @@ import leon.purescala.Trees._
 import leon.purescala.TypeTrees._
 import leon.purescala.TreeOps._
 import leon.purescala.Common._
+import leon.purescala.Definitions._
 import leon.test.purescala.LikelyEq
+import leon.evaluators._
+import leon.LeonContext
 
 import leon.synthesis.LinearEquations._
 
@@ -161,28 +164,30 @@ class LinearEquationsSuite extends LeonTestSuite {
   test("linearSet") {
     val as = Set[Identifier]()
 
+    val evaluator = new DefaultEvaluator(testContext, Program.empty)
+
     val eq1 = Array(3, 4, 8)
-    val basis1 = linearSet(as, eq1)
+    val basis1 = linearSet(evaluator, as, eq1)
     checkVectorSpace(basis1, eq1)
 
     val eq2 = Array(1, 2, 3)
-    val basis2 = linearSet(as, eq2)
+    val basis2 = linearSet(evaluator, as, eq2)
     checkVectorSpace(basis2, eq2)
 
     val eq3 = Array(1, 1)
-    val basis3 = linearSet(as, eq3)
+    val basis3 = linearSet(evaluator, as, eq3)
     checkVectorSpace(basis3, eq3)
 
     val eq4 = Array(1, 1, 2, 7)
-    val basis4 = linearSet(as, eq4)
+    val basis4 = linearSet(evaluator, as, eq4)
     checkVectorSpace(basis4, eq4)
 
     val eq5 = Array(1, -1)
-    val basis5 = linearSet(as, eq5)
+    val basis5 = linearSet(evaluator, as, eq5)
     checkVectorSpace(basis5, eq5)
 
     val eq6 = Array(1, -6, 3)
-    val basis6 = linearSet(as, eq6)
+    val basis6 = linearSet(evaluator, as, eq6)
     checkVectorSpace(basis6, eq6)
   }
 
@@ -215,6 +220,8 @@ class LinearEquationsSuite extends LeonTestSuite {
   test("elimVariable") {
     val as = Set[Identifier](aId, bId)
 
+    val evaluator = new DefaultEvaluator(testContext, Program.empty)
+
     def check(t: Expr, c: List[Expr], prec: Expr, witnesses: List[Expr], freshVars: List[Identifier]) {
       enumerate(freshVars.size, (vals: Array[Int]) => {
         val mapping: Map[Expr, Expr] = (freshVars.zip(vals.toList).map(t => (Variable(t._1), IntLiteral(t._2))).toMap)
@@ -225,28 +232,28 @@ class LinearEquationsSuite extends LeonTestSuite {
 
     val t1 = Minus(Times(IntLiteral(2), a), b)
     val c1 = List(IntLiteral(3), IntLiteral(4), IntLiteral(8))
-    val (pre1, wit1, f1) = elimVariable(as, t1::c1)
+    val (pre1, wit1, f1) = elimVariable(evaluator, as, t1::c1)
     check(t1, c1, pre1, wit1, f1)
 
     val t2 = Plus(Plus(IntLiteral(0), IntLiteral(2)), Times(IntLiteral(-1), IntLiteral(3)))
     val c2 = List(IntLiteral(1), IntLiteral(-1))
-    val (pre2, wit2, f2) = elimVariable(Set(), t2::c2)
+    val (pre2, wit2, f2) = elimVariable(evaluator, Set(), t2::c2)
     check(t2, c2, pre2, wit2, f2)
 
 
     val t3 = Minus(Times(IntLiteral(2), a), IntLiteral(3))
     val c3 = List(IntLiteral(2))
-    val (pre3, wit3, f3) = elimVariable(Set(aId), t3::c3)
+    val (pre3, wit3, f3) = elimVariable(evaluator, Set(aId), t3::c3)
     check(t3, c3, pre3, wit3, f3)
 
     val t4 = Times(IntLiteral(2), a)
     val c4 = List(IntLiteral(2), IntLiteral(4))
-    val (pre4, wit4, f4) = elimVariable(Set(aId), t4::c4)
+    val (pre4, wit4, f4) = elimVariable(evaluator, Set(aId), t4::c4)
     check(t4, c4, pre4, wit4, f4)
 
     val t5 = Minus(a, b)
     val c5 = List(IntLiteral(-60), IntLiteral(-3600))
-    val (pre5, wit5, f5) = elimVariable(Set(aId, bId), t5::c5)
+    val (pre5, wit5, f5) = elimVariable(evaluator, Set(aId, bId), t5::c5)
     check(t5, c5, pre5, wit5, f5)
 
   }
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 46283db481015a1cc7a79d176cbae719398b5e22..408634f9ef596e18046da5cf18659e56e4e8735f 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -25,19 +25,15 @@ class SynthesisRegressionSuite extends LeonTestSuite {
   }
 
   private def testSynthesis(cat: String, f: File, bound: Int) {
-    val ctx = LeonContext(
-      settings = Settings(
+    val ctx = testContext.copy(settings = Settings(
         synthesis = true,
         xlang     = false,
         verify    = false
-      ),
-      files = List(f),
-      reporter = new TestSilentReporter
-    )
+      ))
 
     val opts = SynthesisOptions(searchBound = Some(bound))
 
-    val pipeline = plugin.ExtractionPhase andThen SubtypingPhase
+    val pipeline = plugin.ExtractionPhase andThen leon.utils.SubtypingPhase
 
     val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
 
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 574efa3fe298a405f96604088cb958aff4e152b4..41e0780a4c5f9615ac6be78c2cdf7a0d02761abd 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -25,15 +25,11 @@ class SynthesisSuite extends LeonTestSuite {
 
   def forProgram(title: String)(content: String)(block: (SynthesisContext, FunDef, Problem) => Unit) {
 
-    val ctx = LeonContext(
-      settings = Settings(
+    val ctx = testContext.copy(settings = Settings(
         synthesis = true,
         xlang     = false,
         verify    = false
-      ),
-      files = List(),
-      reporter = new TestSilentReporter
-    )
+      ))
 
     val opts = SynthesisOptions()
 
@@ -55,8 +51,7 @@ class SynthesisSuite extends LeonTestSuite {
                                     program,
                                     solver,
                                     simpleSolver,
-                                    new DefaultReporter,
-                                    new java.util.concurrent.atomic.AtomicBoolean)
+                                    ctx.reporter)
 
         block(sctx, f, p)
       }
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index ea7cc272b15defa10d1f40edd826f4d761b0ec8a..e5692fca09ce6cc1e669192a0e09aad44cf6db8a 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -17,7 +17,7 @@ class PureScalaVerificationRegression extends LeonTestSuite {
   private case class Output(report : VerificationReport, reporter : Reporter)
 
   private def mkPipeline : Pipeline[List[String],VerificationReport] =
-    leon.plugin.ExtractionPhase andThen leon.SubtypingPhase andThen leon.verification.AnalysisPhase
+    leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase andThen leon.verification.AnalysisPhase
 
   private def mkTest(file : File, leonOptions : Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
     val fullName = file.getPath()
@@ -33,15 +33,9 @@ class PureScalaVerificationRegression extends LeonTestSuite {
       assert(file.exists && file.isFile && file.canRead,
              "Benchmark %s is not a readable file".format(displayName))
 
-      val ctx = LeonContext(
-        settings = Settings(
-          synthesis = false,
-          xlang     = false,
-          verify    = true
-        ),
+      val ctx = testContext.copy(
         options = leonOptions.toList,
-        files = List(file),
-        reporter = new TestSilentReporter
+        files   = List(file)
       )
 
       val pipeline = mkPipeline
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 733cafce420e7a33991a621e3184ba5c6fa22bbb..6ddab4332bf0e00305e35ae390bfe92a4e172833 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -17,7 +17,7 @@ class XLangVerificationRegression extends LeonTestSuite {
   private case class Output(report : VerificationReport, reporter : Reporter)
 
   private def mkPipeline : Pipeline[List[String],VerificationReport] =
-    leon.plugin.ExtractionPhase andThen leon.SubtypingPhase andThen xlang.XlangAnalysisPhase
+    leon.plugin.ExtractionPhase andThen leon.utils.SubtypingPhase andThen xlang.XlangAnalysisPhase
 
   private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
     val fullName = file.getPath()
@@ -35,16 +35,7 @@ class XLangVerificationRegression extends LeonTestSuite {
 
       // println("testing " + displayName)
 
-      val ctx = LeonContext(
-        settings = Settings(
-          synthesis = false,
-          xlang     = false,
-          verify    = true
-        ),
-        //options = List(LeonFlagOption("feelinglucky")),
-        files = List(file),
-        reporter = new TestSilentReporter
-      )
+      val ctx = testContext.copy(files = List(file))
 
       val pipeline = mkPipeline