Finished fixing timeouts

src/main/scala/inox/Main.scala

@@ -187,7 +187,8 @@ object Main extends MainHelpers {
         import program.ctx._
 
         import SolverResponses._
-        SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
+        val sf = SolverFactory.default(program).withTimeout(program.ctx.options.findOption(optTimeout))
+        SimpleSolverAPI(sf).solveSAT(expr) match {
           case SatWithModel(model) =>
             reporter.info(" => SAT")
             for ((vd, res) <- model) {

src/main/scala/inox/solvers/package.scala

@@ -47,6 +47,21 @@ package object solvers {
       val program: self.factory.program.type
       type S = self.factory.S { val program: self.factory.program.type }
     } = withTimeout(du.toMillis)
+
+    def withTimeout(optTimeout: Option[Long]): SolverFactory {
+      val program: self.factory.program.type
+      type S = self.factory.S { val program: self.factory.program.type }
+    } = optTimeout match {
+      case Some(to) =>
+        withTimeout(to)
+
+      case None =>
+        // XXX @nv: stupid type checker...
+        factory.asInstanceOf[SolverFactory {
+          val program: self.factory.program.type
+          type S = self.factory.S { val program: self.factory.program.type }
+        }]
+    }
   }
 
 }

src/main/scala/inox/utils/InterruptManager.scala

@@ -47,6 +47,14 @@ class InterruptManager(reporter: Reporter) extends Interruptible {
     }
   }
 
+  def reset() = synchronized {
+    if (isInterrupted) {
+      interrupted.set(false)
+    } else {
+      reporter.warning("Not interrupted!")
+    }
+  }
+
   def registerForInterrupts(i: Interruptible) = synchronized {
     if (isInterrupted) i.interrupt()
     interruptibles.put(i, true)