Fix to help with bug 717

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f9b97d524db54d2a2718e116936f3917c6c5fe73..05094d5a8a635c745325401a61350e9aaf703b03 100644 (file)
--- 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: