From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 9 Jun 2012 17:03:22 +0000 (+0000)
Subject: Turning on unconstrained simp for QF_AUFBV
X-Git-Tag: cvc5-1.0.0~8096
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d1c71026c7b8aaa2e9689d27415d80c412ece2e;p=cvc5.git

Turning on unconstrained simp for QF_AUFBV
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d0f7a0584..e0d507475 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -472,10 +472,12 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
     NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
   }
-  // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
+  // Turn on unconstrained simplification for QF_AUFBV
   if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
-    bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified();
-    bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
+    //    bool qf_sat = d_logic.isPure(theory::THEORY_BOOL) && !d_logic.isQuantified();
+    //    bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
+    bool uncSimp = !Options::current()->incrementalSolving && !d_logic.isQuantified() &&
+      (d_logic.isTheoryEnabled(theory::THEORY_ARRAY) && d_logic.isTheoryEnabled(theory::THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
     NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
   }