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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index ad3eebcefd9c9b11f2c3362c70a5cdbe5f14a5e6..9b713b40bfe0345b24b69ee5f69d2243b4e63888 100644 (file)
--- 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 3893c2e7b20d70551d9d402901e9b16e6dd33d2a..38f39d1ec9cc78b41762cffa2488083383734a18 100644 (file)
--- 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")