From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 29 Oct 2012 13:50:54 +0000 (+0000)
Subject: Disable minisat elimination when models are on
X-Git-Tag: cvc5-1.0.0~7657
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=62988b5d0556d8dd1e0258962d2eaccbe2551281;p=cvc5.git

Disable minisat elimination when models are on
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 55ac15ebc..ca8417dea 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -62,6 +62,7 @@
 #include "theory/model.h"
 #include "printer/printer.h"
 #include "prop/options.h"
+#include "theory/arrays/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -833,12 +834,28 @@ void SmtEngine::setLogicInternal() throw() {
     }
   }
 
-  //until bug 371 is fixed
+  //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
-    if( d_logic.isQuantified() ){
+    if( d_logic.isQuantified() || options::produceModels() ){
       options::minisatUseElim.set( false );
     }
   }
+  else if (options::minisatUseElim()) {
+    if (options::produceModels()) {
+      Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << std::endl;
+      setOption("produce-models", SExpr("false"));
+    }
+    if (options::checkModels()) {
+      Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << std::endl;
+      setOption("check-models", SExpr("false"));
+    }
+  }
+
+  // For now, these array theory optimizations do not support model-building
+  if (options::produceModels()) {
+    options::arraysOptimizeLinear.set(false);
+    options::arraysLazyRIntro1.set(false);
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)