diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index 490b78d7a7f944622d8ec587d64215c41e7cd2e3..0db45b8a0d41e7dcd49f3176bd823a6f3e2eb401 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -147,20 +147,26 @@ object Main extends MainHelpers {
         import program.ctx._
 
         import SolverResponses._
-        SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
+        val error = SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
           case SatWithModel(model) =>
             reporter.info(" => SAT")
             for ((vd, res) <- model) {
               reporter.info(f"${vd.asString}%-15s -> ${res.asString}")
             }
-            exit(error = false)
+            false
           case Unsat =>
             reporter.info(" => UNSAT")
-            exit(error = false)
+            false
           case Unknown =>
             reporter.info(" => UNKNOWN")
-            exit(error = true)
+            true
         }
+
+        reporter.whenDebug(utils.DebugSectionTimers) { debug =>
+          timers.outputTable(debug)
+        }
+
+        exit(error = error)
       }
     }
   }
diff --git a/src/main/scala/inox/utils/Timer.scala b/src/main/scala/inox/utils/Timer.scala
index c334abe9c4f2cc6d596133225008164d047021ab..40088466ab0cd05578daed9bce8561d7d588634e 100644
--- a/src/main/scala/inox/utils/Timer.scala
+++ b/src/main/scala/inox/utils/Timer.scala
@@ -5,6 +5,8 @@ package utils
 
 import scala.language.dynamics
 
+object DebugSectionTimers extends DebugSection("timers")
+
 /** Implements a timer for profiling purposes */
 class Timer() {
   var beginning: Long = 0L