Fixed assertion bug

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 3e0a41591444c770715098e0b1c4bef699020fc9..89f1dbf2c28285e58bd1787ed3fd14a3cc623b09 100644 (file)
--- 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]);