diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index c82a9b0d4dc4c351373e7611ab8bf51ac1ee7abf..fc36dd3ff901e5940a34d6e514376fe1307ff0b4 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -16,7 +16,7 @@ trait SolverFactory {
 
   def shutdown(): Unit = {}
 
-  def reclaim(s: Solver) {
+  def reclaim(s: S) {
     s.free()
   }
 }
diff --git a/src/main/scala/inox/solvers/TimeoutSolver.scala b/src/main/scala/inox/solvers/TimeoutSolver.scala
index 90ce09b793caf0678424eb4783407d27e2949632..3b0d516efa62b143d135511afe32ff9f16cab66c 100644
--- a/src/main/scala/inox/solvers/TimeoutSolver.scala
+++ b/src/main/scala/inox/solvers/TimeoutSolver.scala
@@ -1,14 +1,13 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 
 import utils._
-import purescala.Expressions.Expr
-
 import scala.concurrent.duration._
 
 trait TimeoutSolver extends Solver {
+  import program.trees._
 
   val ti = new TimeoutFor(this)
 
@@ -24,25 +23,26 @@ trait TimeoutSolver extends Solver {
     this
   }
 
-  abstract override def check: Option[Boolean] = {
+  abstract override def check[R](config: Configuration { type Response <: R }): R = {
     optTimeout match {
       case Some(to) =>
         ti.interruptAfter(to) {
-          super.check
+          super.check(config)
         }
       case None =>
-        super.check
+        super.check(config)
     }
   }
 
-  abstract override def checkAssumptions(assumptions: Set[Expr]): Option[Boolean] = {
+  abstract override def checkAssumptions[R](config: Configuration { type Response <: R })
+                                           (assumptions: Set[Expr]): R = {
     optTimeout match {
       case Some(to) =>
         ti.interruptAfter(to) {
-          super.checkAssumptions(assumptions)
+          super.checkAssumptions(config)(assumptions)
         }
       case None =>
-        super.checkAssumptions(assumptions)
+        super.checkAssumptions(config)(assumptions)
     }
   }
 
diff --git a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala b/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
index f3f8ca200f0d8abba7e867a39ebca39d98be2318..b45e5bffae063bd03b109bf2d929b4eaff1db00f 100644
--- a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
+++ b/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
@@ -1,17 +1,26 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 package solvers
 
 import scala.reflect.runtime.universe._
 
-class TimeoutSolverFactory[+S <: TimeoutSolver : TypeTag](val sf: SolverFactory[S], to: Long) extends SolverFactory[S] {
-  override def getNewSolver() = sf.getNewSolver().setTimeout(to)
+trait TimeoutSolverFactory extends SolverFactory {
+  type S <: TimeoutSolver { val program: TimeoutSolverFactory.this.program.type }
 
-  override val name = sf.name+" with t.o"
+  val factory: SolverFactory {
+    val program: TimeoutSolverFactory.this.program.type
+    type S = TimeoutSolverFactory.this.S
+  }
 
-  override def reclaim(s: Solver) = sf.reclaim(s)
+  val to: Long
 
-  override def shutdown() = sf.shutdown()
+  override def getNewSolver() = factory.getNewSolver().setTimeout(to)
+
+  override val name = factory.name+" with t.o"
+
+  override def reclaim(s: S) = factory.reclaim(s)
+
+  override def shutdown() = factory.shutdown()
 }