Fixed bug in array constant normalization found by fuzzer.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index f2632c739..dbbfd04dd 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -94,6 +94,7 @@ class TheoryArraysRewriter {
         // replaced, we can just return node[0]
         return node[0];
       }
+      // else rebuild the store without the replaced write and then exit
     }
     else {
       n = nm->mkNode(kind::STORE, n, index, value);
@@ -106,6 +107,11 @@ class TheoryArraysRewriter {
       elements.pop_back();
     }
 
+    // Ready to exit if write was to the default value (see previous comment)
+    if (value == defaultValue) {
+      return n;
+    }
+
     Cardinality indexCard = index.getType().getCardinality();
     if (indexCard.isInfinite()) {
       return n;