From 35ea6f4cb9b3915d1720b668e98236d453c1d682 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Jan 2022 14:25:19 -0600 Subject: [PATCH] Fix non-idempotent rewrite in arrays (#7887) Fixes #6807. --- src/theory/arrays/theory_arrays_rewriter.cpp | 2 +- src/theory/substitutions.cpp | 2 ++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/arrays/issue6807-idem-rew.smt2 | 8 ++++++++ 4 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/arrays/issue6807-idem-rew.smt2 diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index e933eaacd..5bc0ea176 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -500,7 +500,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) Assert(n != node); Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; - return RewriteResponse(REWRITE_AGAIN, n); + return RewriteResponse(REWRITE_AGAIN_FULL, n); } } break; diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index b56aa4f16..279237eb8 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -213,6 +213,8 @@ Node SubstitutionMap::apply(TNode t, Rewriter* r, std::set* tracker) { if (r != nullptr) { result = r->rewrite(result); + Assert(r->rewrite(result) == result) << "Non-idempotent rewrite: " << result + << " --> " << r->rewrite(result); } return result; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fa3bd1cf8..b3cc02f68 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -109,6 +109,7 @@ set(regress_0_tests regress0/arrays/issue3813-massign-assert.smt2 regress0/arrays/issue3814.smt2 regress0/arrays/issue4927-unsat-cores.smt2 + regress0/arrays/issue6807-idem-rew.smt2 regress0/arrays/issue7596-define-array-uminus.smt2 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2 regress0/arrays/x2.smtv1.smt2 diff --git a/test/regress/regress0/arrays/issue6807-idem-rew.smt2 b/test/regress/regress0/arrays/issue6807-idem-rew.smt2 new file mode 100644 index 000000000..fa226ed11 --- /dev/null +++ b/test/regress/regress0/arrays/issue6807-idem-rew.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun i () Int) +(declare-fun a () (Array Int Int)) +(declare-fun _3 () (Array Int Int)) +(assert (and (= (select a 1) 0) (= _3 (store (store (store a 2 0) 1 1) 0 (select a 0))))) +(assert (= 0 (select (store _3 1 (select a 1)) i))) +(check-sat) -- 2.30.2