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 ca8417deae6bb5f82dc40b52e1fc4186c9ddc47e..7fcb64219cd540dc1b7c063fbd166a84cd40f3ab 100644 (file)
--- 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 );
     }
   }