From 3d1c71026c7b8aaa2e9689d27415d80c412ece2e Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Sat, 9 Jun 2012 17:03:22 +0000 Subject: [PATCH] Turning on unconstrained simp for QF_AUFBV --- src/smt/smt_engine.cpp | 8 +++++--- 1 file 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; } -- 2.30.2