diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 37bedaebf40dfc32a8e84aeea7cc71de2257a095..5601416020877d8417ba1724fea2dbeef8c12aa5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -34,23 +34,25 @@ abstract class SMTLIBSolver(val context: LeonContext,
   extends IncrementalSolver with Interruptible {
 
 
-  // Solver name
+  /* Solver name */
   def targetName: String
   override def name: String = "smt-"+targetName
 
-  // Reporter
+  /* Reporter */
   protected val reporter = context.reporter
 
-  // Interface with Interpreter
+  /* Interface with Interpreter */
+
   def interpreterOps(ctx: LeonContext): Seq[String]
 
   def getNewInterpreter(ctx: LeonContext): SMTInterpreter
 
   protected val interpreter = getNewInterpreter(context)
 
-  protected var out: java.io.FileWriter = _
 
-  reporter.ifDebug { debug =>
+  /* Printing VCs */
+
+  protected val out: java.io.FileWriter = if (reporter.isDebugEnabled) {
     val file = context.files.headOption.map(_.getName).getOrElse("NA")
     val n    = VCNumbers.getNext(targetName+file)
 
@@ -60,14 +62,16 @@ abstract class SMTLIBSolver(val context: LeonContext,
       dir.mkdir
     }
 
-    out = new java.io.FileWriter(s"vcs/$targetName-$file-$n.smt2", false)
-  }
+    new java.io.FileWriter(s"vcs/$targetName-$file-$n.smt2", false)
+  } else null
+
 
+  /* Interruptible interface */
 
-  // Interrupts
   protected var interrupted = false
 
   context.interruptManager.registerForInterrupts(this)
+
   override def interrupt(): Unit = {
     interrupted = true
     interpreter.interrupt()
@@ -76,19 +80,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
     interrupted = false
   }
 
-  override def free() = {
-    interpreter.free()
-    context.interruptManager.unregisterForInterrupts(this)
-    reporter.ifDebug { _ => out.close() }
-  }
-
 
 
+  /*
+   * Translation from Leon Expressions to SMTLIB terms and reverse
+   */
 
-  /** Translation from Leon Expressions etc. */
-
-
-  // Symbols
+  /* Symbol handling */
   protected object SimpleSymbol {
     def unapply(term: Term): Option[SSymbol] = term match {
       case QualifiedIdentifier(SMTIdentifier(sym, Seq()), None) => Some(sym)
@@ -105,7 +103,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
   protected def freshSym(id: Identifier): SSymbol = freshSym(id.name)
   protected def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
 
-  // metadata for CC, and variables
+
+  /* Metadata for CC, and variables */
   protected val constructors  = new IncrementalBijection[TypeTree, SSymbol]()
   protected val selectors     = new IncrementalBijection[(TypeTree, Int), SSymbol]()
   protected val testers       = new IncrementalBijection[TypeTree, SSymbol]()
@@ -117,7 +116,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
   protected def hasError = errors.getB(()) contains true
   protected def addError() = errors += () -> true
 
-  // A manager object for the Option type (since it is hard-coded for Maps)
+  /* A manager object for the Option type (since it is hard-coded for Maps) */
   protected object OptionManager {
     lazy val leonOption = program.library.Option.get
     lazy val leonSome = program.library.Some.get
@@ -166,7 +165,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
   }
 
 
-  // Helpers
+  /* Helper functions */
+
 
   protected def normalizeType(t: TypeTree): TypeTree = t match {
     case ct: ClassType if ct.parent.isDefined => ct.parent.get
@@ -291,7 +291,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
     }
   }
 
-
   protected def getHierarchy(ct: ClassType): (ClassType, Seq[CaseClassType]) = ct match {
     case act: AbstractClassType =>
       (act, act.knownCCDescendents)
@@ -304,7 +303,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
       }
   }
 
-
   protected case class DataType(sym: SSymbol, cases: Seq[Constructor])
   protected case class Constructor(sym: SSymbol, tpe: TypeTree, fields: Seq[(SSymbol, TypeTree)])
 
@@ -478,6 +476,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
     f
   }
 
+  /* Translate a Leon Expr to an SMTLIB term */
+
   protected def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = {
     e match {
       case Variable(id) =>
@@ -708,6 +708,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
     }
   }
 
+  /* Translate an SMTLIB term back to a Leon Expr */
+
   protected def fromSMT(pair: (Term, TypeTree))(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
     fromSMT(pair._1, pair._2)
   }
@@ -800,6 +802,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
       unsupported("Unhandled case in fromSMT: " + (s, tpe))
   }
 
+
+  /* Send a command to the solver */
   def sendCommand(cmd: Command): CommandResponse = {
     reporter.ifDebug { debug =>
       SMTPrinter.printCommand(cmd, out)
@@ -818,7 +822,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
   }
 
 
-  // Public solver interface
+  /* Public solver interface */
+
+  def free() = {
+    interpreter.free()
+    context.interruptManager.unregisterForInterrupts(this)
+    reporter.ifDebug { _ => out.close() }
+  }
 
   override def assertCnstr(expr: Expr): Unit = if(!hasError) {
     variablesOf(expr).foreach(declareVariable)
@@ -831,7 +841,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
         // invocations will return None
         addError()
     }
-
   }
 
   override def check: Option[Boolean] = {