diff options
| -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 e4b9023d5..8f282b413 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1316,9 +1316,9 @@ void SmtEngine::setDefaults() { } else if (options::solveIntAsBV() > 0) { d_logic = LogicInfo("QF_BV"); - // } else if (d_logic.getLogicString() == "QF_UFBV" && - // options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - // d_logic = LogicInfo("QF_BV"); + } else if (d_logic.getLogicString() == "QF_UFBV" && + options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + d_logic = LogicInfo("QF_BV"); } // set strings-exp @@ -3877,8 +3877,8 @@ void SmtEnginePrivate::processAssertions() { } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && - !d_smt.d_logic.isPure(THEORY_BV)) { - // && d_smt.d_logic.getLogicString() != "QF_UFBV") + !d_smt.d_logic.isPure(THEORY_BV) && + d_smt.d_logic.getLogicString() != "QF_UFBV") { throw ModalException("Eager bit-blasting does not currently support theory combination. " "Note that in a QF_BV problem UF symbols can be introduced for division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); |