diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
index 62bd9307881ef29d22e0a3578eb3f8fe84b6aa67..60b148c8cfe106f2e7aaa81cd1277ed714f281f3 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
@@ -18,6 +18,7 @@ trait SMTLIBCVC4CounterExampleTarget extends SMTLIBCVC4QuantifiedTarget {
   override def interpreterOps(ctx: LeonContext) = {
     Seq(
       "-q",
+      "--produce-models",
       "--print-success",
       "--lang", "smt",
       "--fmf-fun"