diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 1e20b15fd13ad664a0f2b47812cf2d45b9126e9b..841a28e50b4c41a560b9f3f33651c4e8b6180f2c 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -3,7 +3,7 @@
 package leon
 package solvers
 
-import utils.{DebugSectionSolver, Interruptible}
+import leon.utils.{Position, DebugSectionSolver, Interruptible}
 import purescala.Expressions._
 import purescala.Common.{Tree, Identifier}
 import purescala.ExprOps._
@@ -87,8 +87,11 @@ trait Solver extends Interruptible {
 
   implicit lazy val leonContext = context
 
+  def dbg(msg: => Any) = context.reporter.debug(msg)
+
   def assertCnstr(expression: Expr): Unit
   def assertVC(vc: VC) = {
+    dbg(s"; Solving $vc @ ${vc.getPos}\n")
     assertCnstr(Not(vc.condition))
   }
 
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 21580d6c2b2f4f263c3e5451396e2b8a7d067a76..b2003d1012dcd35fab90c3cbc3d0f450e505f94b 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -4,7 +4,6 @@ package leon
 package solvers
 package combinators
 
-import purescala.Common._
 import purescala.Expressions._
 import verification.VC
 
@@ -32,6 +31,8 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
     solvers.foreach(_.assertVC(vc))
   }
 
+  override def dbg(msg: => Any) = solvers foreach (_.dbg(msg))
+
   def check: Option[Boolean] = {
     model = Model.empty
 
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
index 8559114554acd2e58566afd948b2d764d38a60b6..7c29a16d0e8965fe0720c0714b3fb2a32598c430 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
@@ -4,8 +4,6 @@ package leon
 package solvers
 package combinators
 
-import utils.Interruptible
-import scala.collection.mutable.Queue
 import scala.reflect.runtime.universe._
 
 class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
diff --git a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
index 2c414f2c0bf9a6f14e6f571b98eed2bfc3ce49aa..0419d7d6e4b2c4064e83d8a03e2a3430d2f70929 100644
--- a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
@@ -4,7 +4,6 @@ package leon
 package solvers
 package combinators
 
-import purescala.Common._
 import purescala.Expressions._
 
 abstract class RewritingSolver[+S <: Solver, T](underlying: S) {
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 6e75a33a9535f5d7eb714acfedde152be64d03fd..0c7afeb65199042e34004199d17bba25dde9e1c5 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -15,7 +15,6 @@ import utils._
 
 import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre}
 import templates._
-import utils.Interruptible
 import evaluators._
 
 class UnrollingSolver(val context: LeonContext, val program: Program, underlying: Solver)
@@ -85,6 +84,8 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
     }
   }
 
+  override def dbg(msg: => Any) = underlying.dbg(msg)
+
   def push() {
     unrollingBank.push()
     solver.push()
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
index bfcb706689062da6659b882c3672bd0e9088d4cd..f98b4f7e45fa71e4456da8ae9934d221feddbbe1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedSolver.scala
@@ -14,6 +14,7 @@ trait SMTLIBQuantifiedSolver {
   // The reason is we do not want to assume postconditions of functions referring to
   // the current function, as this may make the proof unsound
   override def assertVC(vc: VC) = {
+    dbg(s"; Solving $vc")
     currentFunDef = Some(vc.fd)
     assertCnstr(withInductiveHyp(vc.condition))
   }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 05476ac11bd106e1d313695757445ce40b1efd1e..99b4d9d1727144c5d1080dc192d2e6a5e4063f45 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,6 +4,7 @@ package leon
 package solvers
 package smtlib
 
+import verification.VC
 import purescala.Common._
 import purescala.Expressions._
 import purescala.ExprOps._
@@ -23,8 +24,15 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
   /* Reporter */
   protected val reporter = context.reporter
 
+  override def dbg(msg: => Any) = {
+    debugOut foreach { o =>
+      o.write(msg.toString)
+      o.flush()
+    }
+  }
+
   /* Public solver interface */
-  override def assertCnstr(expr: Expr): Unit = if(!hasError) {
+  def assertCnstr(expr: Expr): Unit = if(!hasError) {
     try {
       variablesOf(expr).foreach(declareVariable)
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 9035700a0f12120da6086be426334622017f2b37..01b35d9dec65e1002af734f50eddfd4f5cda5b8b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -24,21 +24,18 @@ import _root_.smtlib.parser.Terms.{
   Let => SMTLet,
   _
 }
-import _root_.smtlib.theories.Core.{
-  Equals => SMTEquals
-}
 import _root_.smtlib.parser.CommandsResponses.{ Error => ErrorResponse, _ }
 import _root_.smtlib.theories._
 import _root_.smtlib.interpreters.ProcessInterpreter
 
 trait SMTLIBTarget extends Interruptible {
-  val context: LeonContext;
-  val program: Program;
-  protected val reporter: Reporter;
+  val context: LeonContext
+  val program: Program
+  protected val reporter: Reporter
 
   def targetName: String
 
-  implicit val debugSection: DebugSection;
+  implicit val debugSection: DebugSection
 
   protected def interpreterOps(ctx: LeonContext): Seq[String]