diff options
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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]); |