From 7d7106f4e62daf77b8ef616a013ea70ebeb24ac0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 27 Nov 2012 17:52:01 +0000 Subject: [PATCH] do not turn on BV for QF_SAT (this commit was certified error- and warning-free by the test-and-commit script.) --- src/smt/smt_engine.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8e6fcccb8..92a339a45 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -963,7 +963,9 @@ void SmtEngine::setLogicInternal() throw() { } // may need to force BV on to handle Boolean terms - if(!d_logic.isPure(theory::THEORY_ARITH)) { + // except in pure arith and QF_SAT + if(!d_logic.isPure(theory::THEORY_ARITH) && + !d_logic.isPure(theory::THEORY_BOOL)) { d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(theory::THEORY_BV); d_logic.lock(); -- 2.30.2