From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 4 Mar 2022 21:50:32 +0000 (+0100)
Subject: Guard recursion into terms during substitution in arithmetic utility (#8234)
X-Git-Tag: cvc5-1.0.0~322
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf155cb1cc523eb0885351d18d8ef0c7b221f38f;p=cvc5.git

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 720ba7478..c1276474b 100644
--- 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 0fc41583d..f1d1de2e8 100644
--- 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
index 000000000..e8f547726
--- /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)