From 1bcf55c6e616aef0aa5de7fea6c5d37588b135a0 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 2 Jun 2022 06:08:43 +0300 Subject: [PATCH] Disable arrays in eager bit-blasting (#8785) Fixes cvc5/cvc5-projects#461 . This does not allow arrays in eager bit-blasting, that is, only QF_BV and QF_UFBV are allowed. The reason is that Ackermannization (which is turned on in eager bit-blasting) eliminates array operators but does not eliminate array variables, that later cause a logic exception. --- src/smt/set_defaults.cpp | 12 +++--------- test/regress/cli/regress0/bv/ackermann3.smt2 | 4 +--- 2 files changed, 4 insertions(+), 12 deletions(-) diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index ad3eebcef..9b713b40b 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -299,12 +299,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const logic.disableTheory(THEORY_UF); logic.lock(); } - if (logic.isTheoryEnabled(THEORY_ARRAYS)) - { - logic = logic.getUnlockedCopy(); - logic.disableTheory(THEORY_ARRAYS); - logic.lock(); - } } // Set default options associated with strings-exp. We also set these options @@ -807,11 +801,11 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const } if (opts.bv.bitblastMode == options::BitblastMode::EAGER - && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV" - && logic.getLogicString() != "QF_ABV") + && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV") { throw OptionException( - "Eager bit-blasting does not currently support theory combination. " + "Eager bit-blasting does not currently support theory combination with " + "any theory other than UF. " "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."); diff --git a/test/regress/cli/regress0/bv/ackermann3.smt2 b/test/regress/cli/regress0/bv/ackermann3.smt2 index 3893c2e7b..38f39d1ec 100644 --- a/test/regress/cli/regress0/bv/ackermann3.smt2 +++ b/test/regress/cli/regress0/bv/ackermann3.smt2 @@ -1,7 +1,5 @@ -; COMMAND-LINE: --bitblast=eager +; COMMAND-LINE: --ackermann ; EXPECT: unsat -; DISABLE-TESTER: unsat-core -; unsat cores throws error in debug (set-logic QF_ABV) (set-info :smt-lib-version 2.6) (set-info :category "crafted") -- 2.30.2