diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 99b4d9d1727144c5d1080dc192d2e6a5e4063f45..f13ed21a2929a0b845e9c0138092bb36b5fc6428 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,7 +4,6 @@ package leon
 package solvers
 package smtlib
 
-import verification.VC
 import purescala.Common._
 import purescala.Expressions._
 import purescala.ExprOps._
@@ -21,9 +20,6 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
   def targetName: String
   override def name: String = "smt-"+targetName
 
-  /* Reporter */
-  protected val reporter = context.reporter
-
   override def dbg(msg: => Any) = {
     debugOut foreach { o =>
       o.write(msg.toString)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 01b35d9dec65e1002af734f50eddfd4f5cda5b8b..33b3a26d88a660fe737b144766c8dfdfa48ff685 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -16,10 +16,15 @@ import purescala.Definitions._
 
 import _root_.smtlib.common._
 import _root_.smtlib.printer.{ RecursivePrinter => SMTPrinter }
-import _root_.smtlib.parser.Commands.{ Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _ }
+import _root_.smtlib.parser.Commands.{
+  Constructor => SMTConstructor,
+  FunDef => _,
+  Assert => _,
+  _
+}
 import _root_.smtlib.parser.Terms.{
   Forall => SMTForall,
-  Exists => SMTExists,
+  Exists => _,
   Identifier => SMTIdentifier,
   Let => SMTLet,
   _
@@ -31,7 +36,7 @@ import _root_.smtlib.interpreters.ProcessInterpreter
 trait SMTLIBTarget extends Interruptible {
   val context: LeonContext
   val program: Program
-  protected val reporter: Reporter
+  protected def reporter = context.reporter
 
   def targetName: String
 
diff --git a/src/main/scala/leon/solvers/sygus/SygusSolver.scala b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
index b0a7f0aab8fdf8f49d5639a5cfc94154a489948f..6d2c7678947c07fb6c53da2beac902e1fb25dbd5 100644
--- a/src/main/scala/leon/solvers/sygus/SygusSolver.scala
+++ b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
@@ -4,24 +4,16 @@ package leon
 package solvers
 package sygus
 
-import utils._
-import grammars._
-
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Types._
 import purescala.ExprOps._
-import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Expressions._
 
-import scala.collection.mutable.ArrayBuffer
-
 import synthesis.Problem
 
 import leon.solvers.smtlib._
 
-import _root_.smtlib.common._
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
 import _root_.smtlib.parser.CommandsResponses.{Error => _, _}
@@ -31,8 +23,6 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p
   implicit val ctx = context
   implicit val debugSection = leon.utils.DebugSectionSynthesis
 
-  val reporter = context.reporter
-
   protected def unsupported(t: Tree, str: String): Nothing = {
     throw new Unsupported(t, str)
   }
diff --git a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
index 7a0e7edf495ef20597e4c9cde1939b5778ebcbbb..7760b8c0d50f0f12958de870311ccba7daa85b22 100644
--- a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
+++ b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
@@ -4,11 +4,9 @@ package leon
 package synthesis
 package rules
 
-import purescala.Types._
 import solvers.sygus._
 
 import grammars._
-import utils._
 
 case object SygusCVC4 extends Rule("SygusCVC4") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {