From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 May 2020 16:47:47 +0000 (-0500)
Subject: Do not enable unconstrained simplification if arithmetic is present (#4489)
X-Git-Tag: cvc5-1.0.0~3320
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b50dfe623f44e97d85449fa2a7566e81c639b47;p=cvc5.git

Do not enable unconstrained simplification if arithmetic is present (#4489)

For now we do not enable unconstrained simplification when arithmetic is present. Post SMT COMP, we should investigate making arithmetic not output lemmas during preprocessing (CVC4/cvc4-wishues#71).
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c887d1895..8236486dd 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -300,7 +300,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
 
   // Disable options incompatible with incremental solving, unsat cores, and
-  // proofs or output an error if enabled explicitly
+  // proofs or output an error if enabled explicitly. It is also currently
+  // incompatible with arithmetic, force the option off.
   if (options::incrementalSolving() || options::unsatCores()
       || options::proof())
   {
@@ -326,8 +327,9 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       bool uncSimp = !logic.isQuantified() && !options::produceModels()
                      && !options::produceAssignments()
                      && !options::checkModels()
-                     && (logic.isTheoryEnabled(THEORY_ARRAYS)
-                         && logic.isTheoryEnabled(THEORY_BV));
+                     && logic.isTheoryEnabled(THEORY_ARRAYS)
+                     && logic.isTheoryEnabled(THEORY_BV)
+                     && !logic.isTheoryEnabled(THEORY_ARITH);
       Trace("smt") << "setting unconstrained simplification to " << uncSimp
                    << std::endl;
       options::unconstrainedSimp.set(uncSimp);