diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-17 17:21:26 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-18 16:39:42 -0400 |
| commit | 066191d91d9f42f34a412162203be818e202aeba (patch) | |
| tree | 10638c91da6e626c90e1a70e85b211852cbca4b5 /src/smt | |
| parent | bd9b95170b21ad066e87a59db78fac8ab7f24629 (diff) | |
Fixes to theoryof-mode; no longer static in Theory class.
Diffstat (limited to 'src/smt')
| -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 |