diff --git a/src/main/scala/inox/solvers/TimeoutSolver.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
similarity index 98%
rename from src/main/scala/inox/solvers/TimeoutSolver.scala
rename to src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
index 17ae644b51c0f009d2efb8e91cb98bd2e1ed14e4..4c74587a08f8d97cca91b80d371464e53f922f2c 100644
--- a/src/main/scala/inox/solvers/TimeoutSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/TimeoutSolver.scala
@@ -2,6 +2,7 @@
 
 package inox
 package solvers
+package combinators
 
 import utils._
 import scala.concurrent.duration._
diff --git a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
similarity index 96%
rename from src/main/scala/inox/solvers/TimeoutSolverFactory.scala
rename to src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
index b45e5bffae063bd03b109bf2d929b4eaff1db00f..0c20fddc9d5ec4112588fb82e627e40ab97ba7fc 100644
--- a/src/main/scala/inox/solvers/TimeoutSolverFactory.scala
+++ b/src/main/scala/inox/solvers/combinators/TimeoutSolverFactory.scala
@@ -2,6 +2,7 @@
 
 package inox
 package solvers
+package combinators
 
 import scala.reflect.runtime.universe._
 
diff --git a/src/main/scala/inox/solvers/package.scala b/src/main/scala/inox/solvers/package.scala
index 34215c07e63f02f33310fa007d2a0b5cc8427667..2fcab5abac35e61c4a9ddc1357cb4133b59f5121 100644
--- a/src/main/scala/inox/solvers/package.scala
+++ b/src/main/scala/inox/solvers/package.scala
@@ -1,22 +1,31 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon
+package inox
 
-import scala.reflect.runtime.universe._
 import scala.concurrent.duration._
 
 package object solvers {
-  implicit class TimeoutableSolverFactory[+S <: TimeoutSolver : TypeTag](val sf: SolverFactory[S]) {
-    def withTimeout(to: Long): TimeoutSolverFactory[S] = {
-      sf match {
-        case tsf: TimeoutSolverFactory[_] =>
-          new TimeoutSolverFactory[S](tsf.sf, to)
-        case _ =>
-          new TimeoutSolverFactory[S](sf, to)
+  import combinators._
+
+  implicit class TimeoutableSolverFactory[S1 <: TimeoutSolver](val sf: SolverFactory { type S = S1 }) {
+    def withTimeout(timeout: Long): TimeoutSolverFactory { type S <: S1 } = {
+      val innerFactory = (sf match {
+        case tsf: TimeoutSolverFactory => tsf.factory
+        case _ => sf
+      }).asInstanceOf[SolverFactory {
+        val program: sf.program.type
+        type S = S1 { val program: sf.program.type }
+      }]
+
+      new TimeoutSolverFactory {
+        val program: sf.program.type = sf.program
+        type S = S1 { val program: sf.program.type }
+        val to = timeout
+        val factory = innerFactory
       }
     }
 
-    def withTimeout(du: Duration): TimeoutSolverFactory[S] = {
+    def withTimeout(du: Duration): TimeoutSolverFactory { type S <: S1 } = {
       withTimeout(du.toMillis)
     }
   }