From cf155cb1cc523eb0885351d18d8ef0c7b221f38f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 4 Mar 2022 22:50:32 +0100 Subject: [PATCH] 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. --- src/theory/arith/nl/equality_substitution.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/issue8161-var-elim.smt2 | 9 +++++++++ 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/nl/issue8161-var-elim.smt2 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 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) -- 2.30.2