diff --git a/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala b/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala
index 41a236fa9835c9037e1a5c73758b142b345e8cff..e17ce6d713fac45ca05c90129918da5f4296ba7c 100644
--- a/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala
+++ b/src/integration/scala/leon/integration/solvers/ModelEnumerationSuite.scala
@@ -7,6 +7,7 @@ import leon.integration.helpers.ExpressionsDSL
 import leon.test._
 import leon._
 import leon.solvers._
+import leon.utils._
 import leon.purescala.Definitions._
 import leon.purescala.Common._
 import leon.evaluators._
@@ -40,7 +41,7 @@ class ModelEnumeratorSuite extends LeonTestSuiteWithProgram with ExpressionsDSL
   )
 
   def getModelEnum(implicit ctx: LeonContext, pgm: Program) = {
-    val sf = SolverFactory.default.asInstanceOf[SolverFactory[IncrementalSolver]]
+    val sf = SolverFactory.default
     new ModelEnumerator(ctx, pgm, sf)
   }
 
diff --git a/src/integration/scala/leon/integration/solvers/TimeoutSolverSuite.scala b/src/integration/scala/leon/integration/solvers/TimeoutSolverSuite.scala
index 6a44bc17c014148462b9405558f0769acd113cc6..cce647cc1eed81df80b6f64d1ffcff2acf9c84aa 100644
--- a/src/integration/scala/leon/integration/solvers/TimeoutSolverSuite.scala
+++ b/src/integration/scala/leon/integration/solvers/TimeoutSolverSuite.scala
@@ -12,7 +12,7 @@ import leon.purescala.Expressions._
 import leon.purescala.Types._
 
 class TimeoutSolverSuite extends LeonTestSuite {
-  private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with Interruptible{
+  private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
     val name = "Idiotic"
     val description = "Loops"
 
@@ -35,6 +35,9 @@ class TimeoutSolverSuite extends LeonTestSuite {
 
     def assertCnstr(e: Expr) = {}
 
+    def push() {}
+    def pop() {}
+
     def free() {}
 
     def reset() {}
diff --git a/src/main/scala/leon/solvers/AssumptionSolver.scala b/src/main/scala/leon/solvers/AssumptionSolver.scala
deleted file mode 100644
index e9f8a9313ef814f3926cdbf7eb95836546b1bee9..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/AssumptionSolver.scala
+++ /dev/null
@@ -1,11 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Expressions.Expr
-
-trait AssumptionSolver extends Solver {
-  def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
-  def getUnsatCore: Set[Expr]
-}
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index e01d8f7edea4caeb9059c70ef68cc48eb8fb085a..3a2db100e7fab9568c5f43618d4104925ec9f735 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -12,7 +12,7 @@ import purescala.ExprOps._
 
 import datagen._
 
-class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with Interruptible with IncrementalSolver with NaiveAssumptionSolver {
+class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
   def name = "Enum"
 
   val maxTried = 10000
diff --git a/src/main/scala/leon/solvers/GroundSolver.scala b/src/main/scala/leon/solvers/GroundSolver.scala
index ad4ab6dc7a290d79f0bddf520b2248a48eb681dc..29ee752383afad17134d7d6aead3eb12c274da72 100644
--- a/src/main/scala/leon/solvers/GroundSolver.scala
+++ b/src/main/scala/leon/solvers/GroundSolver.scala
@@ -14,7 +14,7 @@ import utils.Interruptible
 import utils.IncrementalSeq
 
 // This solver only "solves" ground terms by evaluating them
-class GroundSolver(val context: LeonContext, val program: Program) extends IncrementalSolver with Interruptible {
+class GroundSolver(val context: LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
 
   context.interruptManager.registerForInterrupts(this)
 
diff --git a/src/main/scala/leon/solvers/IncrementalSolver.scala b/src/main/scala/leon/solvers/IncrementalSolver.scala
deleted file mode 100644
index c935558c0a9bfe71f23f7eeef16fe95825022f9c..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/IncrementalSolver.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers
-
-trait IncrementalSolver extends Solver {
-  def push(): Unit
-  def pop(): Unit
-}
-
diff --git a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
index 7c1130b3d549de2428a16a0955ff35dcfab52c71..da1dfa7666a85799607773b967d77489b72b819c 100644
--- a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
@@ -6,8 +6,8 @@ package solvers
 import purescala.Expressions._
 import purescala.Constructors._
 
-trait NaiveAssumptionSolver extends AssumptionSolver {
-  self: IncrementalSolver =>
+trait NaiveAssumptionSolver {
+  self: Solver =>
 
   var lastBs = Set[Expr]()
   def checkAssumptions(bs: Set[Expr]): Option[Boolean] = {
diff --git a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
deleted file mode 100644
index eb92c529cecb1e2ddef88e188ad8de8767efcea8..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
+++ /dev/null
@@ -1,27 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Common.Identifier
-import purescala.Expressions.Expr
-
-class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends SimpleSolverAPI(sf) {
-
-  def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
-    val s = sf.getNewSolver()
-    try {
-      s.assertCnstr(expression)
-      s.checkAssumptions(assumptions) match {
-        case Some(true) =>
-          (Some(true), s.getModel, Set())
-        case Some(false) =>
-          (Some(false), Map(), s.getUnsatCore)
-        case None =>
-          (None, Map(), Set())
-      }
-    } finally {
-      sf.reclaim(s)
-    }
-  }
-}
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index 907f903dfb13207c0568a3d8727fb78d1cc6cc36..37aefc1b5507f087981570b11fe153237d9832de 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -33,16 +33,27 @@ class SimpleSolverAPI(sf: SolverFactory[Solver]) {
       sf.reclaim(s)
     }
   }
+
+  def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
+    val s = sf.getNewSolver()
+    try {
+      s.assertCnstr(expression)
+      s.checkAssumptions(assumptions) match {
+        case Some(true) =>
+          (Some(true), s.getModel, Set())
+        case Some(false) =>
+          (Some(false), Map(), s.getUnsatCore)
+        case None =>
+          (None, Map(), Set())
+      }
+    } finally {
+      sf.reclaim(s)
+    }
+  }
 }
 
 object SimpleSolverAPI {
   def apply(sf: SolverFactory[Solver]) = {
     new SimpleSolverAPI(sf)
   }
-
-  // Wrapping an AssumptionSolver will automatically provide an extended
-  // interface
-  def apply(sf: SolverFactory[AssumptionSolver]) = {
-    new SimpleAssumptionSolverAPI(sf)
-  }
 }
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 54879dcc4b6862bf5c44456d308e89f680a6ccdf..9f8aaace4a8ed890212cc57961471ed2d3a62c00 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -3,12 +3,12 @@
 package leon
 package solvers
 
-import utils.DebugSectionSolver
+import utils.{DebugSectionSolver, Interruptible}
 import purescala.Expressions._
 import purescala.Common.Identifier
 import verification.VC
 
-trait Solver {
+trait Solver extends Interruptible {
   def name: String
   val context: LeonContext
 
@@ -27,6 +27,12 @@ trait Solver {
 
   def reset()
 
+  def push(): Unit
+  def pop(): Unit
+
+  def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
+  def getUnsatCore: Set[Expr]
+
   implicit val debugSection = DebugSectionSolver
 
   private[solvers] def debugS(msg: String) = {
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 6e7273a112f0861588f92330a2f8e3a4e4c3715c..27f4973e024bc25cabba723d8b566e12d055856e 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -41,7 +41,7 @@ object SolverFactory {
     "ground"         -> "Only solves ground verification conditions by evaluating them",
     "enum"           -> "Enumeration-based counter-example-finder"
   )
-  
+
   val availableSolversPretty = "Available: " +
     solvers.SolverFactory.definedSolvers.toSeq.sortBy(_._1).map {
       case (name, desc) =>  f"\n  $name%-14s : $desc"
@@ -76,7 +76,7 @@ object SolverFactory {
     ctx.reporter.fatalError("Aborting Leon...")
   }
 
-  def getFromName(ctx: LeonContext, program: Program)(name: String): SolverFactory[IncrementalSolver with TimeoutSolver] = name match {
+  def getFromName(ctx: LeonContext, program: Program)(name: String): SolverFactory[TimeoutSolver] = name match {
     case "fairz3" =>
       SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
 
diff --git a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
deleted file mode 100644
index 0294d87168b193b92cd8819c1f745f8d31acb4ab..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
+++ /dev/null
@@ -1,21 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers
-
-import purescala.Expressions.Expr
-
-trait TimeoutAssumptionSolver extends TimeoutSolver with AssumptionSolver {
-
-  abstract override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
-    optTimeout match {
-      case Some(to) =>
-        ti.interruptAfter(to) {
-          super.checkAssumptions(assumptions)
-        }
-      case None =>
-        super.checkAssumptions(assumptions)
-    }
-  }
-}
-
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index a7c27f1a0773f40ac9be42a28cfa11811baee894..723b48886dd903f5ac17eb0cad5212a260864659 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -4,10 +4,11 @@ package leon
 package solvers
 
 import utils._
+import purescala.Expressions.Expr
 
 import scala.concurrent.duration._
 
-trait TimeoutSolver extends Solver with Interruptible {
+trait TimeoutSolver extends Solver {
 
   val ti = new TimeoutFor(this)
 
@@ -34,4 +35,15 @@ trait TimeoutSolver extends Solver with Interruptible {
     }
   }
 
+  abstract override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+    optTimeout match {
+      case Some(to) =>
+        ti.interruptAfter(to) {
+          super.checkAssumptions(assumptions)
+        }
+      case None =>
+        super.checkAssumptions(assumptions)
+    }
+  }
+
 }
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
deleted file mode 100644
index ad48ca2cd27604f3106698454febbc5cc1c6faa7..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ /dev/null
@@ -1,138 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package solvers
-package combinators
-
-import purescala.Common._
-import purescala.Constructors._
-import purescala.Expressions._
-import purescala.ExprOps._
-
-class DNFSolver(val context: LeonContext,
-                underlyings: SolverFactory[Solver]) extends Solver {
-
-  def name = "DNF("+underlyings.name+")"
-
-  def free() {}
-
-  private var theConstraint : Option[Expr] = None
-  private var theModel : Option[Map[Identifier,Expr]] = None
-
-  import context.reporter._
-
-  def assertCnstr(expression : Expr) {
-    if(theConstraint.isDefined) { fatalError("Multiple assertCnstr(...).") }
-    theConstraint = Some(expression)
-  }
-
-  def reset() = {
-    throw new CantResetException(this)
-  }
-
-  def check : Option[Boolean] = theConstraint.map { expr =>
-
-    val simpleSolver = SimpleSolverAPI(underlyings)
-
-    var result : Option[Boolean] = None
-
-    debugS("Before NNF:\n" + expr.asString)
-
-    val nnfed = nnf(expr, false)
-
-    debugS("After NNF:\n" + nnfed.asString)
-
-    val dnfed = dnf(nnfed)
-
-    debugS("After DNF:\n" + dnfed.asString)
-
-    val candidates : Seq[Expr] = dnfed match {
-      case Or(es) => es
-      case elze => Seq(elze)
-    }
-
-    debugS("# conjuncts : " + candidates.size)
-
-    var done : Boolean = false
-
-    for(candidate <- candidates if !done) {
-      simpleSolver.solveSAT(candidate) match {
-        case (Some(false), _) =>
-          result = Some(false)
-
-        case (Some(true), m) =>
-          result = Some(true)
-          theModel = Some(m)
-          done = true
-
-        case (None, m) =>
-          result = None
-          theModel = Some(m)
-          done = true
-       }
-    }
-    result
-  } getOrElse {
-    Some(true)
-  }
-
-  def getModel : Map[Identifier,Expr] = {
-    val vs : Set[Identifier] = theConstraint.map(variablesOf).getOrElse(Set.empty)
-    theModel.getOrElse(Map.empty).filter(p => vs(p._1))
-  }
-
-  private def nnf(expr : Expr, flip : Boolean) : Expr = expr match {
-    case _ : Let | _ : IfExpr => throw new Exception("Can't NNF *everything*, sorry.")
-    case Not(Implies(l,r)) => nnf(and(l, not(r)), flip)
-    case Implies(l, r)     => nnf(or(not(l), r), flip)
-    case Not(Equals(l, r)) => nnf(or(and(l, not(r)), and(not(l), r)), flip)
-    case Equals(l, r)      => nnf(or(and(l, r), and(not(l), not(r))), flip)
-    case And(es) if flip   => orJoin(es.map(e  => nnf(e, true)))
-    case And(es)           => andJoin(es.map(e => nnf(e, false)))
-    case Or(es)  if flip   => andJoin(es.map(e => nnf(e, true)))
-    case Or(es)            => orJoin(es.map(e  => nnf(e, false)))
-    case Not(e) if flip    => nnf(e, false)
-    case Not(e)            => nnf(e, true)
-    case LessThan(l,r)      if flip => GreaterEquals(l,r)
-    case GreaterThan(l,r)   if flip => LessEquals(l,r)
-    case LessEquals(l,r)    if flip => GreaterThan(l,r)
-    case GreaterEquals(l,r) if flip => LessThan(l,r)
-    case elze if flip      => not(elze)
-    case elze              => elze
-  }
-
-  private def dnf(expr : Expr) : Expr = expr match {
-    case And(es) =>
-      val (ors, lits) = es.partition(_.isInstanceOf[Or])
-      if(ors.nonEmpty) {
-        val orHead = ors.head.asInstanceOf[Or]
-        val orTail = ors.tail
-        orJoin(orHead.exprs.map(oe => dnf(andJoin(filterObvious(lits ++ (oe +: orTail))))))
-      } else {
-        expr
-      }
-
-    case Or(es) =>
-      orJoin(es.map(dnf))
-
-    case _ => expr
-  }
-
-  private def filterObvious(exprs : Seq[Expr]) : Seq[Expr] = {
-    var pos : List[Identifier] = Nil
-    var neg : List[Identifier] = Nil
-
-    for(e <- exprs) e match {
-      case Variable(id)      => pos = id :: pos
-      case Not(Variable(id)) => neg = id :: neg
-      case _ => ;
-    }
-
-    val both : Set[Identifier] = pos.toSet intersect neg.toSet
-    if(both.nonEmpty) {
-      Seq(BooleanLiteral(false))
-    } else {
-      exprs
-    }
-  }
-}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index ea8331a4adb516ba93b839eb3c13c84141e3e328..9997d5176d0389ad0d0a790e228fbd77cace93b9 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -15,7 +15,7 @@ import scala.concurrent.duration._
 import ExecutionContext.Implicits.global
 
 class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, val solvers: Seq[S])
-        extends Solver with Interruptible {
+        extends Solver with NaiveAssumptionSolver {
 
   val name = "Pfolio"
 
@@ -53,7 +53,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
 
     val result = Future.find(fs)(_._2.isDefined)
 
-    val res = Await.result(result, 10.days) match {
+    val res = Await.result(result, Duration.Inf) match {
       case Some((s, r, m)) =>
         modelMap = m
         resultSolver = s.getResultSolver
@@ -66,10 +66,18 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
         None
     }
 
-    fs map { Await.ready(_, 10.days) }
+    fs map { Await.ready(_, Duration.Inf) }
     res
   }
 
+  def push(): Unit = {
+    solvers.foreach(_.push())
+  }
+
+  def pop(): Unit = {
+    solvers.foreach(_.pop())
+  }
+
   def free() = {
     solvers.foreach(_.free)
     modelMap = Map()
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
index 85c862d297cd2df87d85ec64774a81cecc791df4..8559114554acd2e58566afd948b2d764d38a60b6 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
@@ -8,7 +8,7 @@ import utils.Interruptible
 import scala.collection.mutable.Queue
 import scala.reflect.runtime.universe._
 
-class PortfolioSolverFactory[S <: Solver with Interruptible](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
+class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
 
   def getNewSolver(): PortfolioSolver[S] with TimeoutSolver = {
     new PortfolioSolver[S](ctx, sfs.map(_.getNewSolver())) with TimeoutSolver
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 5bb65cdb3757eb07ebad63e86162dc492cc8ba70..f4bd40885d1b11d4d3924ad8c724874368b0dd8a 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -16,7 +16,7 @@ import templates._
 import utils.Interruptible
 import evaluators._
 
-class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver with Interruptible) extends Solver with Interruptible {
+class UnrollingSolver(val context: LeonContext, program: Program, underlying: Solver) extends Solver with NaiveAssumptionSolver {
 
   val feelingLucky   = context.findOptionOrDefault(optFeelingLucky)
   val useCodeGen     = context.findOptionOrDefault(optUseCodeGen)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 942faa10808624bdb9138920967f1fcfd27e0bf8..3fcaacd4426c8e27f7bc4bdb9955aca53087429b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -30,9 +30,7 @@ import _root_.smtlib.{Interpreter => SMTInterpreter}
 
 
 abstract class SMTLIBSolver(val context: LeonContext,
-                            val program: Program)
-  extends IncrementalSolver with Interruptible {
-
+                            val program: Program) extends Solver with NaiveAssumptionSolver {
 
   /* Solver name */
   def targetName: String
@@ -42,7 +40,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
   protected val reporter = context.reporter
 
   /* Interface with Interpreter */
-
   def interpreterOps(ctx: LeonContext): Seq[String]
 
   def getNewInterpreter(ctx: LeonContext): SMTInterpreter
@@ -51,7 +48,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
 
   /* Printing VCs */
-
   protected lazy val out: Option[java.io.FileWriter] = if (reporter.isDebugEnabled) Some {
     val file = context.files.headOption.map(_.getName).getOrElse("NA")
     val n    = VCNumbers.getNext(targetName+file)
@@ -62,9 +58,9 @@ abstract class SMTLIBSolver(val context: LeonContext,
       dir.mkdir
     }
 
-    val fileName = s"vcs/$targetName-$file-$n.smt2"
+    val fileName = s"smt-sessions/$targetName-$file-$n.smt2"
 
-    reporter.debug(s"Outputting VC into $fileName" )
+    reporter.debug(s"Outputting smt session into $fileName" )
 
     val fw = new java.io.FileWriter(fileName, false)
 
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 550e84f057f6c5d49f139325a5bbdfaf74ac29f4..b2683eb588cdabcd5baaedd20e0c4e8300e0bd50 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -21,11 +21,7 @@ import scala.collection.mutable.{Map => MutableMap}
 
 // This is just to factor out the things that are common in "classes that deal
 // with a Z3 instance"
-trait AbstractZ3Solver
-  extends Solver
-     with AssumptionSolver
-     with IncrementalSolver 
-     with Interruptible {
+trait AbstractZ3Solver extends Solver {
 
   val context : LeonContext
   val program : Program
diff --git a/src/main/scala/leon/solvers/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
similarity index 74%
rename from src/main/scala/leon/solvers/ModelEnumerator.scala
rename to src/main/scala/leon/utils/ModelEnumerator.scala
index 3a5fdc5dfcbb7d63f5d8d261e73a96a55f87cc49..e813d8b504ad7b462a811ddd48ad66091cd17885 100644
--- a/src/main/scala/leon/solvers/ModelEnumerator.scala
+++ b/src/main/scala/leon/utils/ModelEnumerator.scala
@@ -1,5 +1,5 @@
 package leon
-package solvers
+package utils
 
 import purescala.Definitions._
 import purescala.Common._
@@ -8,14 +8,14 @@ import purescala.Constructors._
 import purescala.ExprOps._
 import purescala.Types._
 import evaluators._
+import solvers._
 
-
-class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[IncrementalSolver]) {
+class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) {
   private[this] var reclaimPool = List[Solver]()
   private[this] val evaluator = new DefaultEvaluator(ctx, pgm)
 
-  def enumSimple(ids: Seq[Identifier], cnstr: Expr): Iterator[Map[Identifier, Expr]] = {
-    enumVarying0(ids, cnstr, None, -1)
+  def enumSimple(ids: Seq[Identifier], satisfying: Expr): Iterator[Map[Identifier, Expr]] = {
+    enumVarying0(ids, satisfying, None, -1)
   }
 
   /**
@@ -25,26 +25,26 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Incremen
    * Note: there is no guarantee that the models enumerated consecutively share the
    * same `caracteristic`.
    */
-  def enumVarying(ids: Seq[Identifier], cnstr: Expr, caracteristic: Expr, nPerCaracteristic: Int = 1) = {
-    enumVarying0(ids, cnstr, Some(caracteristic), nPerCaracteristic)
+  def enumVarying(ids: Seq[Identifier], satisfying: Expr, measure: Expr, nPerMeasure: Int = 1) = {
+    enumVarying0(ids, satisfying, Some(measure), nPerMeasure)
   }
 
-  private[this] def enumVarying0(ids: Seq[Identifier], cnstr: Expr, caracteristic: Option[Expr], nPerCaracteristic: Int = 1): Iterator[Map[Identifier, Expr]] = {
+  private[this] def enumVarying0(ids: Seq[Identifier], satisfying: Expr, measure: Option[Expr], nPerMeasure: Int = 1): Iterator[Map[Identifier, Expr]] = {
     val s = sf.getNewSolver
     reclaimPool ::= s
 
-    s.assertCnstr(cnstr)
+    s.assertCnstr(satisfying)
 
-    val c = caracteristic match {
-      case Some(car) =>
-        val c = FreshIdentifier("car", car.getType)
-        s.assertCnstr(Equals(c.toVariable, car))
-        c
+    val m = measure match {
+      case Some(ms) =>
+        val m = FreshIdentifier("measure", ms.getType)
+        s.assertCnstr(Equals(m.toVariable, ms))
+        m
       case None =>
         FreshIdentifier("noop", BooleanType)
     }
 
-    var perCarRemaining = Map[Expr, Int]()
+    var perMeasureRem = Map[Expr, Int]().withDefaultValue(nPerMeasure)
 
     new Iterator[Map[Identifier, Expr]] {
       def hasNext = {
@@ -53,27 +53,28 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Incremen
 
       def next = {
         val sm = s.getModel
-        val m = (ids.map { id =>
+        val model = (ids.map { id =>
           id -> sm.getOrElse(id, simplestValue(id.getType))
         }).toMap
 
 
         // Vary the model
-        s.assertCnstr(not(andJoin(m.toSeq.sortBy(_._1).map { case (k,v) => equality(k.toVariable, v) })))
+        s.assertCnstr(not(andJoin(model.toSeq.sortBy(_._1).map { case (k,v) => equality(k.toVariable, v) })))
 
-        caracteristic match {
-          case Some(car) =>
-            val cValue = evaluator.eval(car, m).result.get
+        measure match {
+          case Some(ms) =>
+            val mValue = evaluator.eval(ms, model).result.get
 
-            perCarRemaining += (cValue -> (perCarRemaining.getOrElse(cValue, nPerCaracteristic) - 1))
-            if (perCarRemaining(cValue) == 0) {
-              s.assertCnstr(not(equality(c.toVariable, cValue)))
+            perMeasureRem += (mValue -> (perMeasureRem(mValue) - 1))
+
+            if (perMeasureRem(mValue) <= 0) {
+              s.assertCnstr(not(equality(m.toVariable, mValue)))
             }
 
           case None =>
         }
 
-        m
+        model
       }
     }
   }
@@ -90,13 +91,13 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Incremen
   case object Up   extends SearchDirection
   case object Down extends SearchDirection
 
-  private[this] def enumOptimizing(ids: Seq[Identifier], cnstr: Expr, measure: Expr, dir: SearchDirection): Iterator[Map[Identifier, Expr]] = {
+  private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): Iterator[Map[Identifier, Expr]] = {
     assert(measure.getType == IntegerType)
 
     val s = sf.getNewSolver
     reclaimPool ::= s
 
-    s.assertCnstr(cnstr)
+    s.assertCnstr(satisfying)
 
     val mId = FreshIdentifier("measure", measure.getType)
     s.assertCnstr(Equals(mId.toVariable, measure))
diff --git a/src/test/scala/leon/test/solvers/SolverPoolSuite.scala b/src/test/scala/leon/test/solvers/SolverPoolSuite.scala
index 04d4d77237273cdd5c4bcdbf8e2e24dd0d523ace..b733ee193a7500f2edd4e2b1719a0e05c7ecfc7b 100644
--- a/src/test/scala/leon/test/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/leon/test/solvers/SolverPoolSuite.scala
@@ -12,7 +12,7 @@ import leon.purescala.Expressions._
 
 class SolverPoolSuite extends LeonTestSuite {
 
-  private class DummySolver(val context : LeonContext, val program: Program) extends Solver {
+  private class DummySolver(val context : LeonContext, val program: Program) extends Solver with NaiveAssumptionSolver {
     val name = "Dummy"
     val description = "dummy"
 
@@ -21,6 +21,10 @@ class SolverPoolSuite extends LeonTestSuite {
     def free() {}
     def reset() {}
     def getModel = ???
+    def push() {}
+    def pop() {}
+    def interrupt() {}
+    def recoverInterrupt() {}
   }
 
   def sfactory(implicit ctx: LeonContext): SolverFactory[Solver] = {