Turning on unconstrained simp for QF_AUFBV

1 files changed, 5 insertions, 3 deletions

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;
   }