From 75c6e785cf9173a27c9d367f16c85e1889e245d5 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 13 Nov 2012 01:24:27 +0000
Subject: [PATCH] Fixed bug in array constant normalization found by fuzzer.

---
 src/theory/arrays/theory_arrays_rewriter.h | 6 ++++++
 1 file changed, 6 insertions(+)

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;
-- 
2.30.2