diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-11-15 20:52:09 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-11-15 20:52:09 +0000 |
| commit | 263ec763ab08a137b7997c7b2c536a22aa6496f6 (patch) | |
| tree | 654e09d6303993dddf5f4418b27f15031fecd3ec /src/smt | |
| parent | a0e91c27c047e7abcfd254584e8a9f27c676b9ed (diff) | |
changed logic options so that justification is turned on for QF_ABV and QF_UFBV as well
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 16de7957a..69aec695c 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); @@ -848,10 +848,10 @@ void SmtEngine::setLogicInternal() throw() { (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV) ) || - // QF_AUFBV + // QF_AUFBV or QF_ABV or QF_UFBV (not d_logic.isQuantified() && - d_logic.isTheoryEnabled(THEORY_ARRAY) && - d_logic.isTheoryEnabled(THEORY_UF) && + (d_logic.isTheoryEnabled(THEORY_ARRAY) || + d_logic.isTheoryEnabled(THEORY_UF)) && d_logic.isTheoryEnabled(THEORY_BV) ) || // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?) |