Fix VC numbering, options, and solver names.

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",

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",

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
 

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"

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
+  }
+}