From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 29 Oct 2012 18:25:48 +0000 (+0000)
Subject: Tweak to options configuration for turning off minisat elimination when models are on
X-Git-Tag: cvc5-1.0.0~7656
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45d96ce6cdd0eb5a899611b4b0be243c6887da39;p=cvc5.git

Tweak to options configuration for turning off minisat elimination when models are on
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ca8417dea..7fcb64219 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -836,7 +836,7 @@ void SmtEngine::setLogicInternal() throw() {
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
-    if( d_logic.isQuantified() || options::produceModels() ){
+    if( d_logic.isQuantified() || options::produceModels() || options::checkModels() ){
       options::minisatUseElim.set( false );
     }
   }