diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index fec39a7c14f539577237a8dc76187dcb6b95367b..31056406ccb586f16178aff0e2e94df6b4d451c3 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -77,19 +77,19 @@ object SolverFactory {
         SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
 
       case "smt-z3" =>
-        SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBZ3Target(ctx, program)) with TimeoutSolver)
+        SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
 
       case "smt-z3-q" =>
-        SolverFactory(() => new SMTLIBZ3QuantifiedTarget(ctx, program) with TimeoutSolver)
+        SolverFactory(() => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
 
       case "smt-cvc4" =>
-        SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBCVC4Target(ctx, program)) with TimeoutSolver)
+        SolverFactory(() => new UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
 
       case "smt-cvc4-proof" =>
-        SolverFactory(() => new SMTLIBCVC4ProofTarget(ctx, program) with TimeoutSolver)
+        SolverFactory(() => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
 
       case "smt-cvc4-cex" =>
-        SolverFactory(() => new SMTLIBCVC4CounterExampleTarget(ctx, program) with TimeoutSolver)
+        SolverFactory(() => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
 
       case _ =>
         ctx.reporter.error(s"Unknown solver $name")
@@ -127,7 +127,7 @@ object SolverFactory {
         ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-based solver.")
         reported = true
       }
-      SolverFactory(() => new SMTLIBZ3Target(ctx, program) with TimeoutSolver)
+      SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
     }
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
similarity index 73%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index d3e9c0008793616b730a9b25e1a89e13c022bb45..6a42646e6e749170fd60b037cfa21e76152e7931 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -5,7 +5,7 @@ package solvers.smtlib
 
 import purescala.Definitions.Program
 
-class SMTLIBCVC4CounterExampleTarget(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedTarget(context, program) {
+class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
 
   override val targetName = "cvc4-cex"
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
similarity index 79%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 4d6b4d1ca1215dd18bffe80078afd095e8411cbc..32bc12b4eef27df8f5ff2c5d1bff722b492899ff 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -5,7 +5,7 @@ package solvers.smtlib
 
 import leon.purescala.Definitions.Program
 
-class SMTLIBCVC4ProofTarget(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedTarget(context, program) {
+class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
 
   override val targetName = "cvc4-proof"
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
similarity index 96%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 9ac752c744a7cef72833cc8841c9aac61d159cf0..f5de0bb3448a4de5dee8bbc1844df3bc6de644d5 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -14,7 +14,7 @@ import smtlib.theories.Core.Equals
 
 // This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
 // It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
-abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBCVC4Target(context, program) {
+abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBCVC4Solver(context, program) {
 
   override val targetName = "cvc4-quantified"
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
similarity index 99%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 80930ba43ab4903837313cbfcaf48f00a2c85688..69d12b68607fa486ca15e813a592b84d3ea014dc 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -19,7 +19,7 @@ import _root_.smtlib.parser.Commands._
 import _root_.smtlib.interpreters.CVC4Interpreter
 import _root_.smtlib.theories._
 
-class SMTLIBCVC4Target(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
+class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
 
   def targetName = "cvc4"
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
similarity index 93%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index 041f52260b12e73e71f6c1ef00256584b4d1dff4..7e8dd06733c2846871f8cacfafa9bd10a70ff9a8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -13,7 +13,7 @@ import smtlib.parser.Terms.{ForAll => SMTForall, SSymbol}
  * This solver models function definitions as universally quantified formulas.
  * It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
  */
-class SMTLIBZ3QuantifiedTarget(context: LeonContext, program: Program) extends SMTLIBZ3Target(context, program) {
+class SMTLIBZ3QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBZ3Solver(context, program) {
 
   private val typedFunDefExplorationLimit = 10000
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
similarity index 99%
rename from src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
rename to src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index d7565c8d55c852aafb303afcc3baabb3a44ca686..1fb33303f6db9961d08d4b705ce22cae8aa404b8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -20,7 +20,7 @@ import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess
 import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
 import _root_.smtlib.theories.ArraysEx
 
-class SMTLIBZ3Target(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
+class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolver(context, program) {
 
   def targetName = "z3"