summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/smt/smt_engine.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e1d247521..6567a775b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -458,7 +458,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
// Set the options for the theoryOf
if(!Options::current()->theoryOfModeSetByUser) {
- if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV) && !d_logic.isQuantified()) {
+ if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
Theory::setTheoryOfMode(theory::THEORY_OF_TERM_BASED);
} else {
Theory::setTheoryOfMode(theory::THEORY_OF_TYPE_BASED);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback