From: Clark Barrett Date: Wed, 8 May 2013 15:25:14 +0000 (-0400) Subject: Fixed assertion bug X-Git-Tag: cvc5-1.0.0~7287^2~138 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f8927c16764151ed217b509a60e22336a2981de;p=cvc5.git Fixed assertion bug --- 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]);