From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 13 Nov 2012 01:24:27 +0000 (+0000)
Subject: Fixed bug in array constant normalization found by fuzzer.
X-Git-Tag: cvc5-1.0.0~7612
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75c6e785cf9173a27c9d367f16c85e1889e245d5;p=cvc5.git

Fixed bug in array constant normalization found by fuzzer.
---

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;