From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 6 Jan 2022 20:25:19 +0000 (-0600)
Subject: Fix non-idempotent rewrite in arrays (#7887)
X-Git-Tag: cvc5-1.0.0~592
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35ea6f4cb9b3915d1720b668e98236d453c1d682;p=cvc5.git

Fix non-idempotent rewrite in arrays (#7887)

Fixes #6807.
---

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<TNode>* 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)