Disable minisat variable elimination when a parametric theory is present (#8487)

Fixes cvc5/cvc5-projects#506.

It seems there are extremely few cases where it is safe to use this option.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 32fafc75b7f12fb3ba1a1cf5f4d33c95a1adb68f..b3a8007a13ae792eb0c4a103b8084953d59adc52 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -695,12 +695,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       && opts.prop.minisatSimpMode == options::MinisatSimpMode::ALL)
   {
     // cannot use minisat variable elimination for logics where a theory solver
-    // introduces new literals into the search. This includes quantifiers
+    // introduces new literals into the search, or for parametric theories
+    // which may introduce Boolean term variables. This includes quantifiers
     // (quantifier instantiation), and the lemma schemas used in non-linear
     // and sets. We also can't use it if models are enabled.
     if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS)
-        || logic.isQuantified() || opts.smt.produceModels
-        || opts.smt.produceAssignments || opts.smt.checkModels
+        || logic.isTheoryEnabled(THEORY_ARRAYS)
+        || logic.isTheoryEnabled(THEORY_STRINGS)
+        || logic.isTheoryEnabled(THEORY_DATATYPES) || logic.isQuantified()
+        || opts.smt.produceModels || opts.smt.produceAssignments
+        || opts.smt.checkModels
         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
     {
       opts.prop.minisatSimpMode = options::MinisatSimpMode::CLAUSE_ELIM;

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index f20bc9edde5ca5d4b00b37fc81526105e937bca6..f4c318da4d12fc7260f594170d67d954a0a8d31b 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -132,6 +132,7 @@ set(regress_0_tests
   regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/issue8103-1-weak-equiv-models.smt2
   regress0/arrays/issue8276-arith-getModelValue.smt2
+  regress0/arrays/proj-issue506-ms-var-elim.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2

diff --git a/test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2 b/test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2
new file mode 100644 (file)
index 0000000..4097491
--- /dev/null
+++ b/test/regress/cli/regress0/arrays/proj-issue506-ms-var-elim.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_AX)
+(set-info :status sat)
+(declare-const x (Array Bool Bool))
+(declare-const _x Bool)
+(assert (select (store x _x false) false))
+(check-sat)