diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
similarity index 88%
rename from src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
rename to src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
index 8bea481be9db15fe816a2c2680cdc5a4a49cfb52..02306d21936bbeb34adb428ef13bec8903c8d6cd 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Solver.scala
@@ -6,9 +6,9 @@ package smtlib
 
 import inox.OptionParsers._
 
-class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
+class CVC4Solver(val program: Program, val options: SolverOptions)
   extends SMTLIBSolver
-     with SMTLIBCVC4Target {
+     with CVC4Target {
 
   protected val userDefinedOps = {
     options.findOptionOrDefault(optCVC4Options)
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
similarity index 99%
rename from src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala
rename to src/main/scala/inox/solvers/smtlib/CVC4Target.scala
index a263a30422c7ab27a47e6826ebce03b911499c03..3936ea8733e810a510f018686a610ebafe7118ed 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
@@ -12,7 +12,7 @@ import _root_.smtlib.interpreters.CVC4Interpreter
 import _root_.smtlib.theories.experimental.Sets
 import _root_.smtlib.theories.experimental.Strings
 
-trait SMTLIBCVC4Target extends SMTLIBTarget {
+trait CVC4Target extends SMTLIBTarget {
   import program._
   import trees._
   import symbols._
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
similarity index 53%
rename from src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala
rename to src/main/scala/inox/solvers/smtlib/Z3Solver.scala
index 223097df4c0084ab362130b6c8e91e8f3ae6703a..64b5b127f0486728df72cf7a34a8a9ec4c30f2c2 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Solver.scala
@@ -4,6 +4,6 @@ package inox
 package solvers
 package smtlib
 
-class SMTLIBZ3Solver(val program: Program, val options: SolverOptions)
+class Z3Solver(val program: Program, val options: SolverOptions)
   extends SMTLIBSolver
-     with SMTLIBZ3Target
+     with Z3Target
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
similarity index 99%
rename from src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala
rename to src/main/scala/inox/solvers/smtlib/Z3Target.scala
index d0868974106d4334a23e024c2103f56ce8993c17..2a59c4a97804b6b0a59689257f1089da6da0ed9e 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
@@ -10,7 +10,7 @@ import _root_.smtlib.interpreters.Z3Interpreter
 import _root_.smtlib.theories.Core.{Equals => SMTEquals, _}
 import _root_.smtlib.theories._
 
-trait SMTLIBZ3Target extends SMTLIBTarget {
+trait Z3Target extends SMTLIBTarget {
 
   import program._
   import trees._