From 3f8927c16764151ed217b509a60e22336a2981de Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 8 May 2013 11:25:14 -0400
Subject: [PATCH] Fixed assertion bug

---
 src/theory/arrays/theory_arrays.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3e0a41591..89f1dbf2c 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -464,7 +464,9 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   }
   case kind::STORE: {
     // Invariant: array terms should be preregistered before being added to the equality engine
-    Assert(!d_equalityEngine.hasTerm(node));
+    if (d_equalityEngine.hasTerm(node)) {
+      break;
+    }
     d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
 
     TNode a = d_equalityEngine.getRepresentative(node[0]);
-- 
2.30.2