From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 25 Apr 2022 19:00:51 +0000 (-0500)
Subject: Option exception for quantified bit-vectors + eager bitblasting + incremental (#8658)
X-Git-Tag: cvc5-1.0.1~228
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=329700eb5c88e984bd3fccef77fe5f13511233f0;p=cvc5.git

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 50404dccb..9acdec976 100644
--- 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 9dc8e67ce..3b2c18688 100644
--- 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
index 000000000..2404260cc
--- /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)