diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-27 14:28:24 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-05-27 14:28:24 -0700 |
| commit | d058f9aacac64bbe384995e81af92cb8b2bb032d (patch) | |
| tree | 968c920c4d8e50ad66f9aa4d9d1ccc1f1e2e2567 /src/smt/smt_engine.cpp | |
| parent | 4592171ab9c8d3653766d19ec73f4e7f39cf9e17 (diff) | |
Enabled bit-blasting option for QF_UFBV
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -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."); |