diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala
index 5b71c18546b5081263549438cd03167b684f5aa2..c85ed8688d578e091a1cc040f7f5897f766f8449 100644
--- a/src/main/scala/inox/solvers/Solver.scala
+++ b/src/main/scala/inox/solvers/Solver.scala
@@ -4,7 +4,6 @@ package inox
 package solvers
 
 import utils._
-import evaluators._
 
 case class SolverOptions(options: Seq[InoxOption[Any]]) extends InoxOptions[SolverOptions] {
   def build(opts: Seq[InoxOption[Any]]): SolverOptions = SolverOptions(opts)
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
index 16311ecbf4b7f31bde58ff1cbd45cc00b4057efc..8bea481be9db15fe816a2c2680cdc5a4a49cfb52 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -4,10 +4,16 @@ package inox
 package solvers
 package smtlib
 
+import inox.OptionParsers._
+
 class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
   extends SMTLIBSolver
      with SMTLIBCVC4Target {
 
+  protected val userDefinedOps = {
+    options.findOptionOrDefault(optCVC4Options)
+  }
+
   def interpreterOps(ctx: InoxContext) = {
     Seq(
       "-q",
@@ -17,6 +23,14 @@ class SMTLIBCVC4Solver(val program: Program, val options: SolverOptions)
       "--rewrite-divk",
       "--print-success",
       "--lang", "smt2.5"
-    )
+    ) ++ userDefinedOps.toSeq
   }
 }
+
+object optCVC4Options extends InoxOptionDef[Set[String]] {
+  val name = "solver:cvc4"
+  val description = "Pass extra arguments to CVC4"
+  val default = Set[String]()
+  val parser = setParser(stringParser)
+  val usageRhs = "<cvc4-opt>"
+}