Implement a bad version of printing vc position in SMT file

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))
   }
 

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
 

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] {

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) {

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()

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))
   }

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)
 

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]