From 0ae4a52735412cf874ee28abe648fba8a4c51a70 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 6 May 2015 14:42:32 +0200
Subject: [PATCH] Produce models in CEX solver

---
 .../leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala     | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
index 62bd93078..60b148c8c 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"
-- 
GitLab