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 e933eaacd07884c373a633ad9ad42be635afa8d6..5bc0ea176263ab364942a395ca75b421d88c8b28 100644 (file)
--- 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 b56aa4f16265d282c2130e5c0bc92d39a35422b8..279237eb845d5c4d511ead4c0c4539cb6f4f3e34 100644 (file)
--- 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 fa3bd1cf8a293a74666dd02e844d4f1886c9cefd..b3cc02f6809f736a69695e4070296bb6f79b210b 100644 (file)
--- 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 (file)
index 0000000..fa226ed
--- /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)