From d058f9aacac64bbe384995e81af92cb8b2bb032d Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 27 May 2016 14:28:24 -0700 Subject: [PATCH] Enabled bit-blasting option for QF_UFBV --- src/smt/smt_engine.cpp | 10 +++++----- 1 file 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."); -- 2.30.2