From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 29 May 2018 17:46:35 +0000 (-0500)
Subject: Disable minisat elimination when nonlinear is enabled (#2006)
X-Git-Tag: cvc5-1.0.0~5000
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=908158f6833e3765b18041076187ed4cd8004a85;p=cvc5.git

Disable minisat elimination when nonlinear is enabled (#2006)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9d4462210..6ecf00ccd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2196,8 +2196,15 @@ void SmtEngine::setDefaults() {
 
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
-    //AJR: cannot use minisat elim for new implementation of sets TODO: why?
-    if( d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
+    // cannot use minisat elimination for logics where a theory solver
+    // introduces new literals into the search. This includes quantifiers
+    // (quantifier instantiation), and the lemma schemas used in non-linear
+    // and sets. We also can't use it if models are enabled.
+    if (d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified()
+        || options::produceModels() || options::produceAssignments()
+        || options::checkModels()
+        || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()))
+    {
       options::minisatUseElim.set( false );
     }
   }