Always check legal eliminations in quantified logics (#6720)

Fixes #6699.

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index d6ad4cd4116f684f680e6604490fcc9dee1f54a8..b9dc1ba42871ecd9393452266d7b64493f0f3e3a 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -330,12 +330,18 @@ bool Theory::isLegalElimination(TNode x, TNode val)
   {
     return false;
   }
-  if (!options::produceModels())
+  if (!options::produceModels() && !d_logicInfo.isQuantified())
   {
-    // don't care about the model, we are fine
+    // Don't care about the model and logic is not quantified, we can eliminate.
     return true;
   }
-  // if there is a model object
+  // If models are enabled, then it depends on whether the term contains any
+  // unevaluable operators like FORALL, SINE, etc. Having such operators makes
+  // model construction contain non-constant values for variables, which is
+  // not ideal from a user perspective.
+  // We also insist on this check since the term to eliminate should never
+  // contain quantifiers, or else variable shadowing issues may arise.
+  // there should be a model object
   TheoryModel* tm = d_valuation.getModel();
   Assert(tm != nullptr);
   return tm->isLegalElimination(x, val);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ca281af7b97e2077ec6ee1c6638538d5999ada08..6706ed4f68688a04c1c6edb41c315d0f07077dbd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1614,13 +1614,10 @@ set(regress_1_tests
   regress1/ho/issue4065-no-rep.smt2
   regress1/ho/issue4092-sinf.smt2
   regress1/ho/issue4134-sinf.smt2
-  regress1/ho/nested_lambdas-AGT034^2.smt2
-  regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
   regress1/ho/NUM638^1.smt2
   regress1/ho/NUM925^1.p
   regress1/ho/soundness_fmf_SYO362^5-delta.p
   regress1/ho/store-ax-min.p
-  regress1/ho/SYO056^1.p
   regress1/hole6.cvc
   regress1/ite5.smt2
   regress1/issue3970-nl-ext-purify.smt2
@@ -1849,6 +1846,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5658-qe.smt2
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
   regress1/quantifiers/issue5899-qe.smt2
+  regress1/quantifiers/issue6699-nc-shadow.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
@@ -2632,6 +2630,10 @@ set(regression_disabled_tests
   regress1/fmf/ko-bound-set.cvc
   # results in an assertion failure (see issue #1650).
   regress1/ho/hoa0102.smt2
+  # after disallowing solving for terms with quantifiers
+  regress1/ho/nested_lambdas-AGT034^2.smt2
+  regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
+  regress1/ho/SYO056^1.p
   # slow on some builds after changes to tangent planes
   regress1/nl/approx-sqrt-unsat.smt2
   # times out after update to circuit propagator

diff --git a/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2 b/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2
new file mode 100644 (file)
index 0000000..e1e0cdb
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue6699-nc-shadow.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -i
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun v1 () Bool)
+(declare-fun v4 () Bool)
+(declare-fun v7 () Bool)
+(assert (distinct v7 v1 (and v4 (exists ((q1 Int)) (= (= 0 q1) (and v7 v1))))))
+(push)
+(check-sat)