diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 6a42646e6e749170fd60b037cfa21e76152e7931..361806c2d398e47550ce84da921d695d22deeaf0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
@@ -7,11 +7,12 @@ import purescala.Definitions.Program
 
 class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
 
-  override val targetName = "cvc4-cex"
+  override def targetName = "cvc4-cex"
 
   override def interpreterOps(ctx: LeonContext) = {
     Seq(
       "-q",
+      "--rewrite-divk",
       "--produce-models",
       "--print-success",
       "--lang", "smt",
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 32bc12b4eef27df8f5ff2c5d1bff722b492899ff..678d5915fb38c0693be593b9baf90e3ee4453850 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -7,7 +7,7 @@ import leon.purescala.Definitions.Program
 
 class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
 
-  override val targetName = "cvc4-proof"
+  override def targetName = "cvc4-proof"
 
   override def interpreterOps(ctx: LeonContext) = {
     Seq(
@@ -15,6 +15,7 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
       "--print-success",
       "--lang", "smt",
       "--quant-ind",
+      "--rewrite-divk",
       "--conjecture-gen",
       "--conjecture-gen-per-round=3",
       "--conjecture-gen-gt-enum=40",
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index f5de0bb3448a4de5dee8bbc1844df3bc6de644d5..3bdc59d2556c528f74715d78b806d0118939a3b2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -16,7 +16,7 @@ import smtlib.theories.Core.Equals
 // It is not meant as an underlying solver to UnrollingSolver, and does not handle HOFs.
 abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program) extends SMTLIBCVC4Solver(context, program) {
 
-  override val targetName = "cvc4-quantified"
+  override def targetName = "cvc4-quantified"
 
   private val typedFunDefExplorationLimit = 10000
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index 69d12b68607fa486ca15e813a592b84d3ea014dc..cfc92dc44ede4f7acf61371fd50e652e86bfee5c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -33,6 +33,7 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
       "--produce-models",
       "--no-incremental",
       "--tear-down-incremental",
+      "--rewrite-divk",
 //      "--dt-rewrite-error-sel", // Removing since it causes CVC4 to segfault on some inputs
       "--print-success",
       "--lang", "smt"
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 37e5908dc093b6461214bde2d3edce7f5bd1a517..37bedaebf40dfc32a8e84aeea7cc71de2257a095 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -87,15 +87,6 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
   /** Translation from Leon Expressions etc. */
 
-  // Unique numbers
-  protected object VCNumbers {
-    private var nexts = Map[String, Int]().withDefaultValue(0)
-    def getNext(id: String) = {
-      val n = nexts(id)+1
-      nexts += id -> n
-      n
-    }
-  }
 
   // Symbols
   protected object SimpleSymbol {
@@ -904,3 +895,12 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
 }
 
+// Unique numbers
+protected object VCNumbers {
+  private var nexts = Map[String, Int]().withDefaultValue(0)
+  def getNext(id: String) = {
+    val n = nexts(id)+1
+    nexts += id -> n
+    n
+  }
+}