diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2017-03-18 13:46:37 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.stanford.edu> | 2017-03-18 13:46:37 -0700 |
| commit | ab8ef0b914bfc9d434d3569fda9538e628e9f207 (patch) | |
| tree | 176ec8d847c7348bb51c11dddcd857980c2c6c64 /src/theory/arrays | |
| parent | 768534c0973788cab0097c6485e5113da1d406da (diff) | |
Fix to help with bug 717
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f9b97d524..05094d5a8 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -354,10 +354,11 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs case kind::NOT: { d_ppFacts.push_back(in); - Assert(in[0].getKind() == kind::EQUAL ); - Node a = in[0][0]; - Node b = in[0][1]; - d_ppEqualityEngine.assertEquality(in[0], false, in); + if (in[0].getKind() == kind::EQUAL ) { + Node a = in[0][0]; + Node b = in[0][1]; + d_ppEqualityEngine.assertEquality(in[0], false, in); + } break; } default: |