From: Clark Barrett <barrett@cs.stanford.edu>
Date: Sat, 18 Mar 2017 20:46:37 +0000 (-0700)
Subject: Fix to help with bug 717
X-Git-Tag: cvc5-1.0.0~5882
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ab8ef0b914bfc9d434d3569fda9538e628e9f207;p=cvc5.git

Fix to help with bug 717
---

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: