Guard recursion into terms during substitution in arithmetic utility (#8234)

This PR fixes an issue during variable elimination using equalities in the nonlinear arithmetic solver. We need to make sure that we don't apply the substitutions within terms that are not native arithmetic terms. While we already did that whenever we actually used the resulting term, we did not when we just checked for a possible loop.
Although we always invalidate the substitution cache, the apply method also poisons the actual substitution map. By protecting the calls to apply where we don't actually store the result as well, we avoid this type of "poisoning".
Fixes #8161.

diff --git a/src/theory/arith/nl/equality_substitution.cpp b/src/theory/arith/nl/equality_substitution.cpp
index 720ba7478398dd3d1e69e3c9b80eee08ee3e0346..c1276474b80fb4777215e3e12b3b19cb2cbf323d 100644 (file)
--- a/src/theory/arith/nl/equality_substitution.cpp
+++ b/src/theory/arith/nl/equality_substitution.cpp
@@ -90,7 +90,7 @@ std::vector<Node> EqualitySubstitution::eliminateEqualities(
         if (d_substitutions->hasSubstitution(l)) continue;
         if (expr::hasSubterm(r, l)) continue;
         d_substitutions->invalidateCache();
-        if (expr::hasSubterm(d_substitutions->apply(r), l)) continue;
+        if (expr::hasSubterm(d_substitutions->apply(r, nullptr, nullptr, &stc), l)) continue;
         Trace("nl-eqs") << "Found substitution " << l << " -> " << r
                         << std::endl
                         << " from " << o << " / " << orig << std::endl;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0fc41583d2377ffa215cd3b150fccf66016c99ab..f1d1de2e809d92c24516aa189a4ca7efdab2a1de 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -781,6 +781,7 @@ set(regress_0_tests
   regress0/nl/issue6547-ran-model.smt2
   regress0/nl/issue6619-ran-model.smt2
   regress0/nl/issue8135-icp-candidates.smt2
+  regress0/nl/issue8161-var-elim.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2

diff --git a/test/regress/regress0/nl/issue8161-var-elim.smt2 b/test/regress/regress0/nl/issue8161-var-elim.smt2
new file mode 100644 (file)
index 0000000..e8f5477
--- /dev/null
+++ b/test/regress/regress0/nl/issue8161-var-elim.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-fun r5 () Real)
+(declare-fun r7 () Real)
+(declare-fun r26 () Real)
+(assert (or (= 3 r5) (= r7 0)))
+(assert (and (< r26 0.0) (< r7 r26)))
+(assert (or (> r5 1) (= 0.0 (/ (- r26 (/ r5 0.0)) r7))))
+(check-sat)