diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index c6be43a6275b08bf5e67c0dfd30f6a11e8512151..09ac0e7fa3920650f43fb4830e5b1aeacdf41615 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -140,34 +140,34 @@ object Main extends MainHelpers {
     if (files.isEmpty) {
       ctx.reporter.fatalError(s"Input file was not specified.\nTry the --help option for more information.")
     } else {
-      for (file <- files) {
-        val (syms, expr) = new tip.Parser(file).parseScript
+      var error: Boolean = false
+      for (file <- files;
+           (syms, expr) <- new tip.Parser(file).parseScript) {
         val program = InoxProgram(ctx, syms)
         import program._
         import program.ctx._
 
         import SolverResponses._
-        val error = SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
+        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}")
             }
-            false
           case Unsat =>
             reporter.info(" => UNSAT")
-            false
           case Unknown =>
             reporter.info(" => UNKNOWN")
-            true
+            error = true
         }
 
-        reporter.whenDebug(utils.DebugSectionTimers) { debug =>
-          timers.outputTable(debug)
-        }
+      }
 
-        exit(error = error)
+      ctx.reporter.whenDebug(utils.DebugSectionTimers) { debug =>
+        ctx.timers.outputTable(debug)
       }
+
+      exit(error = error)
     }
   }
 }
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
index 37eaca9f6b02364e7cef9a8e7a448f60b00813ab..2fecf82f63cebeb707f065ef805ea6cc31cc8099 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
@@ -4,6 +4,7 @@ package inox
 package solvers
 package smtlib
 
+import utils._
 import _root_.smtlib.parser.Terms._
 
 trait SMTLIBDebugger extends SMTLIBTarget {
@@ -48,3 +49,6 @@ trait SMTLIBDebugger extends SMTLIBTarget {
     super.emit(cmd, rawOut = rawOut)
   }
 }
+
+// Unique numbers
+private[smtlib] object DebugFileNumbers extends UniqueCounter[String]
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index 9688bafd584f54e453cd81f3ef32a04e529a0b71..f0265459700f5b81fde1c7f65fb741d1a94d3e52 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -729,6 +729,3 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
     fromSMT(s, Some(tpe))
   }
 }
-
-// Unique numbers
-private[smtlib] object DebugFileNumbers extends UniqueCounter[String]
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 6cde5ecec1dbef4ccbe5d9ba59c96467940b9b92..f73e2f58556fae8a9519664e27ec3542e4ffb28f 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -33,21 +33,24 @@ class Parser(file: File) {
     pos.map(p => positions.get(p.line, p.col)).getOrElse(NoPosition)
   }
 
-  def parseScript: (Symbols, Expr) = {
+  def parseScript: Seq[(Symbols, Expr)] = {
     val parser = new TipParser(new TipLexer(positions.reader))
     val script = parser.parseScript
 
     var assertions: Seq[Expr] = Seq.empty
     implicit var locals: Locals = NoLocals
 
-    for (cmd <- script.commands) {
-      val (newAssertions, newLocals) = extractCommand(cmd)
-      assertions ++= newAssertions
-      locals = newLocals
-    }
-
-    val expr: Expr = locals.symbols.andJoin(assertions)
-    (locals.symbols, expr)
+    (for (cmd <- script.commands) yield cmd match {
+      case CheckSat() =>
+        val expr: Expr = locals.symbols.andJoin(assertions)
+        Some((locals.symbols, expr))
+
+      case _ =>
+        val (newAssertions, newLocals) = extractCommand(cmd)
+        assertions ++= newAssertions
+        locals = newLocals
+        None
+    }).flatten
   }
 
   protected class Locals (
diff --git a/src/main/scala/inox/tip/TipDebugger.scala b/src/main/scala/inox/tip/TipDebugger.scala
new file mode 100644
index 0000000000000000000000000000000000000000..806d83e983c9cdbee91af7ffbb9452552d91214b
--- /dev/null
+++ b/src/main/scala/inox/tip/TipDebugger.scala
@@ -0,0 +1,38 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import utils._
+import solvers._
+
+trait TipDebugger extends Solver {
+  import program._
+
+  implicit val debugSection: DebugSection
+
+  abstract override def free(): Unit = {
+    super.free()
+    debugOut.foreach(_.close())
+  }
+
+  protected lazy val debugOut: Option[java.io.FileWriter] = {
+    if (ctx.reporter.isDebugEnabled) {
+      val file = ctx.options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
+      val n = DebugFileNumbers.next(file)
+      val fileName = s"tip-sessions/$file-$n.tip"
+
+      val javaFile = new java.io.File(fileName)
+      javaFile.getParentFile.mkdirs()
+
+      ctx.reporter.debug(s"Outputting tip session into $fileName")
+      val fw = new java.io.FileWriter(javaFile, false)
+      Some(fw)
+    } else {
+      None
+    }
+  }
+}
+
+// Unique numbers
+private[tip] object DebugFileNumbers extends UniqueCounter[String]