Option exception for quantified bit-vectors + eager bitblasting + incremental (#8658)

Fixes #8654.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 50404dccb67dcd57ff61663752b1282eba3858c5..9acdec976956dc7f37760633ded057880db36b40 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -230,8 +230,16 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
     }
     else if (!opts.base.incrementalSolving)
     {
+      // if not incremental, we rely on ackermann to eliminate other theories.
       opts.smt.ackermann = true;
     }
+    else if (logic.isQuantified() || !logic.isPure(THEORY_BV))
+    {
+      // requested bitblast=eager in incremental mode, must be QF_BV only.
+      throw OptionException(
+          std::string("Eager bit-blasting is only support in incremental mode "
+                      "if the logic is quantifier-free bit-vectors"));
+    }
   }
 
   if (opts.smt.solveIntAsBV > 0)
@@ -284,6 +292,8 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
     }
     notifyModifyOption("ackermann", "false", "model generation");
     opts.smt.ackermann = false;
+    // we are not relying on ackermann to eliminate theories in this case
+    Assert(opts.bv.bitblastMode != options::BitblastMode::EAGER);
   }
 
   if (opts.smt.ackermann)

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 9dc8e67cea721d0b660a0e8d1e52b9515881cfe7..3b2c18688b678c18cfe84dc904dcf1af12ce3180 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -458,6 +458,7 @@ set(regress_0_tests
   regress0/bv/issue5396.smt2
   regress0/bv/issue8159-1-rewrite-bvneg.smt2
   regress0/bv/issue8240-rewrite-bvnot.smt2
+  regress0/bv/issue8654-bitblast-quant-exc.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2

diff --git a/test/regress/cli/regress0/bv/issue8654-bitblast-quant-exc.smt2 b/test/regress/cli/regress0/bv/issue8654-bitblast-quant-exc.smt2
new file mode 100644 (file)
index 0000000..2404260
--- /dev/null
+++ b/test/regress/cli/regress0/bv/issue8654-bitblast-quant-exc.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed -e 's/(error.*/error/'
+; COMMAND-LINE: -i --bitblast=eager
+; EXPECT: error
+; EXIT: 1
+(set-logic BV)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(assert (forall ((c Bool) (d Bool)) (or (and a d) (and b d) (and c d))))
+(check-sat)