diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 17:52:01 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 17:52:01 +0000 |
| commit | 7d7106f4e62daf77b8ef616a013ea70ebeb24ac0 (patch) | |
| tree | cfab61d49a5b2dd92dc1834a11d3728799ac751c | |
| parent | 41fc06dc6352a847f047970e63e46455eb4dd050 (diff) | |
do not turn on BV for QF_SAT
(this commit was certified error- and warning-free by the test-and-commit script.)
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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(); |