diff --git a/src/main/scala/leon/solvers/IncrementalSolver.scala b/src/main/scala/leon/solvers/IncrementalSolver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8a8e5de49efde3657c4da59dbd218a9b9189cd6e
--- /dev/null
+++ b/src/main/scala/leon/solvers/IncrementalSolver.scala
@@ -0,0 +1,72 @@
+package leon
+package solvers
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.TreeOps._
+import purescala.Trees._
+
+trait IncrementalSolverBuilder {
+  def getNewSolver: IncrementalSolver
+}
+
+trait IncrementalSolver {
+  // New Solver API
+  // Moslty for z3 solvers since z3 4.3
+
+  def push(): Unit
+  def pop(lvl: Int = 1): Unit
+  def assertCnstr(expression: Expr): Unit
+
+  def check: Option[Boolean]
+  def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean]
+  def getModel: Map[Identifier, Expr]
+  def getUnsatCore: Set[Expr]
+}
+
+trait NaiveIncrementalSolver extends IncrementalSolverBuilder {
+  def solveSAT(e: Expr): (Option[Boolean], Map[Identifier, Expr])
+
+  def getNewSolver = new IncrementalSolver {
+    private var stack = List[List[Expr]]()
+
+    def push() {
+      stack = Nil :: stack
+    }
+
+    def pop(lvl: Int = 1) {
+      stack = stack.drop(lvl)
+    }
+
+    def assertCnstr(expression: Expr) {
+      stack = (expression :: stack.head) :: stack.tail
+    }
+
+    private def allConstraints() = stack.flatten
+
+    private var unsatCore = Set[Expr]()
+
+    def check: Option[Boolean] = {
+      solveSAT(And(allConstraints()))._1
+    }
+
+    def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
+      solveSAT(And(assumptions ++ allConstraints()))._1 match {
+        case Some(true) =>
+          unsatCore = Set[Expr]()
+          Some(true)
+        case r =>
+          unsatCore = assumptions.toSet
+          r
+      }
+    }
+
+    def getModel: Map[Identifier, Expr] = {
+      Map[Identifier, Expr]()
+    }
+
+    def getUnsatCore: Set[Expr] = {
+      unsatCore
+    }
+  }
+}
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index 3bc724c68873238e6ef8195cb5410b1ee83c6ffe..3ecf8df6f5b0298be7e91d900168f85c9f22a252 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -15,7 +15,7 @@ import scala.actors.Actor._
 import scala.concurrent.Lock
 
 @deprecated("Unused, Untested, Unmaintained", "")
-class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) {
+class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with NaiveIncrementalSolver {
   private val nbSolvers = solvers.size
   require(nbSolvers >= 2)
 
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index f5e37ca29936f7bd874416674996930eb02f3ab7..fead03a79312bdc78903cef84f6f9ed501180912 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -12,7 +12,7 @@ import Evaluator._
 import scala.util.Random
 
 @deprecated("Unused, Untested, Unmaintained", "")
-class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extends Solver(context) {
+class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extends Solver(context) with NaiveIncrementalSolver {
   require(nbTrial.forall(i => i >= 0))
 
   private val reporter = context.reporter
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 7afbff9b20a7bade166b969e58781c2821522024..0cd3dcac0fec3b7b7b27ae0355c1f42f14a96ef7 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -6,7 +6,7 @@ import purescala.Definitions._
 import purescala.TreeOps._
 import purescala.Trees._
 
-abstract class Solver(val context : LeonContext) {
+abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder {
   // This used to be in Extension
   val description : String
   val shortDescription : String
@@ -55,47 +55,5 @@ abstract class Solver(val context : LeonContext) {
   }
 
   protected def forceStop = _forceStop
-
-  // New Solver API
-  // Moslty for z3 solvers since z3 4.3
-  private var stack = List[List[Expr]](Nil)
-  def push() {
-    stack = Nil :: stack
-  }
-
-  def pop(lvl: Int = 1) {
-    stack = stack.drop(lvl)
-  }
-
-  def assertCnstr(expression: Expr) {
-    stack = (expression :: stack.head) :: stack.tail
-  }
-
-  private def allConstraints() = stack.flatten
-
-  def check: Option[Boolean] = {
-    solveSAT(And(allConstraints()))._1
-  }
-
-  private var unsatCore = Set[Expr]()
-
-  def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
-    solveSAT(And(assumptions ++ allConstraints()))._1 match {
-      case Some(true) =>
-        unsatCore = Set[Expr]()
-        Some(true)
-      case r =>
-        unsatCore = assumptions.toSet
-        r
-    }
-  }
-
-  def getModel: Map[Identifier, Expr] = {
-    Map[Identifier, Expr]()
-  }
-
-  def getUnsatCore: Set[Expr] = {
-    unsatCore
-  }
 }
 
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 2c1de0e4b2be7603d7b9a42c1bc6eeca857f505d..8f1f18ad1d2d8b2ba44a4528b278a40d9acdd00d 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -8,7 +8,7 @@ import purescala.TypeTrees._
 
 import scala.sys.error
 
-class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.context) {
+class TimeoutSolver(solver : Solver, timeout : Int) extends Solver(solver.context) with NaiveIncrementalSolver {
 
   val description = solver.description + ", with timeout"
   override val shortDescription = solver.shortDescription + "+t"
diff --git a/src/main/scala/leon/solvers/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index 17fac01f03f856d487d1d393c16aaa5dce355a52..bd8edcf50903d83ced6dc06f3021f2806b9cb484 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -6,7 +6,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-class TrivialSolver(context: LeonContext) extends Solver(context) {
+class TrivialSolver(context: LeonContext) extends Solver(context) with NaiveIncrementalSolver {
   val description = "Solver for syntactically trivial formulas"
   override val shortDescription = "trivial"
 
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 99349648434acb1047ac31d6328a16bd865a5d77..bfcec027cc5ae3a0ebee65277c9f403d16194d92 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -13,7 +13,7 @@ import scala.collection.mutable.{Set => MutableSet}
 
 // This is just to factor out the things that are common in "classes that deal
 // with a Z3 instance"
-trait AbstractZ3Solver {
+trait AbstractZ3Solver extends solvers.IncrementalSolverBuilder {
   self: leon.solvers.Solver =>
 
   val context : LeonContext
@@ -96,25 +96,6 @@ trait AbstractZ3Solver {
     }
   }
 
-  override def push() {
-    solver.push
-  }
-
-  override def pop(lvl: Int = 1) {
-    solver.pop(lvl)
-  }
-
-  override def assertCnstr(expression: Expr) {
-    solver.assertCnstr(toZ3Formula(expression).get)
-  }
-
-  override def check: Option[Boolean] = {
-    solver.check
-  }
-
-  override def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
-    solver.checkAssumptions(assumptions.map(toZ3Formula(_).get) : _*)
-  }
 
   protected[leon] def restartZ3 : Unit = {
     counter = 0
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 93c0e8e737940685eb043b2974cee965da38b29e..0660dd26ce43fd2410786b8156449a7307a67ef6 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -160,19 +160,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
     }
   }
 
-  override def getModel = {
-    modelToMap(solver.getModel, varsInVC)
-  }
-
-  override def getUnsatCore = {
-    solver.getUnsatCore.map(ast => fromZ3Formula(null, ast, None) match {
-      case n @ Not(Variable(_)) => n
-      case v @ Variable(_) => v
-      case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
-    }).toSet
-  }
-
-
   override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
     restartZ3
     decideWithModel(expression, false, None, Some(assumptions))
@@ -703,5 +690,44 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
 
     }
   }
+
+  def getNewSolver = new solvers.IncrementalSolver {
+    val solver = z3.mkSolver
+
+    def push() {
+      solver.push
+    }
+
+    def pop(lvl: Int = 1) {
+      solver.pop(lvl)
+    }
+
+    def assertCnstr(expression: Expr) {
+      solver.assertCnstr(toZ3Formula(expression).get)
+    }
+
+    def check: Option[Boolean] = {
+      solver.check
+    }
+
+    def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
+      solver.checkAssumptions(assumptions.map(toZ3Formula(_).get) : _*)
+    }
+
+    def getModel = {
+      modelToMap(solver.getModel, varsInVC)
+    }
+
+    def getUnsatCore = {
+      solver.getUnsatCore.map(ast => fromZ3Formula(null, ast, None) match {
+        case n @ Not(Variable(_)) => n
+        case v @ Variable(_) => v
+        case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
+      }).toSet
+    }
+
+
+  }
+
 }
 
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 9215e6c40aceaf9e273265e5370b5058c7794880..2d40fcf1da0859685f8ef39b9270d080adb71728 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -80,4 +80,46 @@ class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with
 
     result
   }
+
+  def getNewSolver = new solvers.IncrementalSolver {
+    val solver = z3.mkSolver
+
+    def push() {
+      solver.push
+    }
+
+    def pop(lvl: Int = 1) {
+      solver.pop(lvl)
+    }
+
+    private var variables = Set[Identifier]()
+
+    def assertCnstr(expression: Expr) {
+      variables ++= variablesOf(expression)
+      solver.assertCnstr(toZ3Formula(expression).get)
+    }
+
+    def check: Option[Boolean] = {
+      solver.check
+    }
+
+    def checkAssumptions(assumptions: Seq[Expr]): Option[Boolean] = {
+      variables ++= assumptions.flatMap(variablesOf(_))
+      solver.checkAssumptions(assumptions.map(toZ3Formula(_).get) : _*)
+    }
+
+    def getModel = {
+      modelToMap(solver.getModel, variables)
+    }
+
+    def getUnsatCore = {
+      solver.getUnsatCore.map(ast => fromZ3Formula(null, ast, None) match {
+        case n @ Not(Variable(_)) => n
+        case v @ Variable(_) => v
+        case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")")
+      }).toSet
+    }
+
+
+  }
 }