From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 2 Apr 2013 03:06:13 +0000 (-0400)
Subject: Fix regression error by turning off model-based solver when models are on
X-Git-Tag: cvc5-1.0.0~7343
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f51b6e9a9dc853156ee392c26f40494d91f345e9;p=cvc5.git

Fix regression error by turning off model-based solver when models are on
(ironic, yes, but model-based solver doesn't yet produce models)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7bbc12551..de41a34a0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -874,11 +874,13 @@ void SmtEngine::setLogicInternal() throw() {
       options::arraysEagerIndexSplitting.set(false);
     }
   }
-  // Turn on model-based arrays for QF_AX
+  // Turn on model-based arrays for QF_AX (unless models are enabled)
   if(! options::arraysModelBased.wasSetByUser()) {
     if (not d_logic.isQuantified() &&
         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-        d_logic.isPure(THEORY_ARRAY)) {
+        d_logic.isPure(THEORY_ARRAY) &&
+        !options::produceModels() &&
+        !options::checkModels()) {
       Trace("smt") << "turning on model-based array solver" << endl;
       options::arraysModelBased.set(true);
     }