diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6e09408d9..b2a0ba771 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -835,12 +835,9 @@ void SmtEngine::setLogicInternal() throw() { // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { - Theory::setTheoryOfMode(THEORY_OF_TERM_BASED); - } else { - Theory::setTheoryOfMode(THEORY_OF_TYPE_BASED); + Trace("smt") << "setting theoryof-mode to term-based" << endl; + options::theoryOfMode.set(THEORY_OF_TERM_BASED); } - } else { - Theory::setTheoryOfMode(options::theoryOfMode()); } // by default, symmetry breaker is on only for QF_UF |