projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
41fc06d
)
do not turn on BV for QF_SAT
author
Morgan Deters
<mdeters@gmail.com>
Tue, 27 Nov 2012 17:52:01 +0000
(17:52 +0000)
committer
Morgan Deters
<mdeters@gmail.com>
Tue, 27 Nov 2012 17:52:01 +0000
(17:52 +0000)
(this commit was certified error- and warning-free by the test-and-commit script.)
src/smt/smt_engine.cpp
patch
|
blob
|
history
diff --git
a/src/smt/smt_engine.cpp
b/src/smt/smt_engine.cpp
index 8e6fcccb8957c0b39793ba2a64d9f7975d075fd7..92a339a45a8a43812cdf7269c85b2c92b55ee2c1 100644
(file)
--- 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();