From ab8ef0b914bfc9d434d3569fda9538e628e9f207 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Sat, 18 Mar 2017 13:46:37 -0700 Subject: [PATCH] Fix to help with bug 717 --- src/theory/arrays/theory_arrays.cpp | 9 +++++---- 1 file 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: -- 2.30.2