diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
index 361806c2d398e47550ce84da921d695d22deeaf0..19bf277410fff3e9bf76e23afd9e9c8a9c8df4cb 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleSolver.scala
+++ b/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
 }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index fc4d8a1ebd47024ebf3d3a4494397612d6446d61..e02c0dfc9a1f454003200a0d717211e061a659d6 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/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
 }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 9a949a6d7e153355bd5357ae21d0d2546a83b89f..70903557b589d07851fc1dfc556a74b3b25affb9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/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)