diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 17:06:08 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-13 17:06:08 +0000 |
| commit | 095d208d95a682ac63b80a059b1a0900e676759f (patch) | |
| tree | 5b73fab65455b6727445b39309a4705f3bf71bc9 /src | |
| parent | b5e8317b54db8c68281ab6889e8ec7ad21270876 (diff) | |
Fixed failing assertion when EqualityEngine is in conflict
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 0cd487d32..9717f6286 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -359,6 +359,9 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) { */ void TheoryArrays::preRegisterTerm(TNode node) { + if (d_conflict) { + return; + } Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; switch (node.getKind()) { case kind::EQUAL: |