diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-05-08 11:25:14 -0400 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-05-08 11:25:26 -0400 |
| commit | 3f8927c16764151ed217b509a60e22336a2981de (patch) | |
| tree | 4556c88b26e8e63dc5a2f105e9f87a57c3bb63b5 | |
| parent | 3b1f1148158efbb8e1785754baf1465776c39eae (diff) | |
Fixed assertion bug
| -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]); |