No forall in cvc4-cex

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala

@@ -20,4 +20,5 @@ class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) ext
     ) ++ userDefinedOps(ctx)
   }
 
+  val allowQuantifiedAssersions: Boolean = false
 }

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala

@@ -54,4 +54,6 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
         other
     }
   }
+
+  protected val allowQuantifiedAssersions: Boolean = true
 }

src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala

@@ -29,6 +29,8 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
 
   private val typedFunDefExplorationLimit = 10000
 
+  protected val allowQuantifiedAssersions: Boolean
+
   override def declareFunction(tfd: TypedFunDef): SSymbol = {
     val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
     if (!exploredAll) {
@@ -94,7 +96,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
     if (smtFunDecls.nonEmpty) {
       sendCommand(DefineFunsRec(smtFunDecls, smtBodies))
       // Assert contracts for defined functions
-      for {
+      if (allowQuantifiedAssersions) for {
         // If we encounter a function that does not refer to the current function,
         // it is sound to assume its contracts for all inputs
         tfd <- withParams if !refersToCurrent(tfd.fd)