diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-11-15 20:57:22 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-15 20:57:22 +0000 |
| commit | 88ef1f0be6bd712cf1ce8401416d634f61f381b4 (patch) | |
| tree | 6d247ecf3a09d2a34be18dc20d1be73df5f973ca /src/smt | |
| parent | 263ec763ab08a137b7997c7b2c536a22aa6496f6 (diff) | |
forgot to uncomment setLogicInternal for THEORY_BV
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 69aec695c..425892583 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -720,8 +720,8 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); // may need to force uninterpreted functions to be on for non-linear - if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) /*|| - d_logic.isTheoryEnabled(theory::THEORY_BV)*/) && + if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) || + d_logic.isTheoryEnabled(theory::THEORY_BV)) && !d_logic.isTheoryEnabled(theory::THEORY_UF)){ d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(theory::THEORY_UF); |