fixing the wrong results. arrays equality adaptor had a missing case when propagating disequalities between shared terms.

1 files changed, 10 insertions, 3 deletions

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 6592e86cf..3ae0146c1 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -243,7 +243,7 @@ class TheoryArrays : public Theory {
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl;
+      Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         if (t1.getType().isArray()) {
           d_arrays.mergeArrays(t1, t2);
@@ -253,9 +253,16 @@ class TheoryArrays : public Theory {
         }
         // Propagate equality between shared terms
         Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        d_arrays.propagate(equality);
+        return d_arrays.propagate(equality);
+      } else {
+        if (t1.getType().isArray()) {
+          if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
+            return true;
+          }
+        }
+        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+        return d_arrays.propagate(equality.notNode());
       }
-      // TODO: implement negation propagation
       return true;
     }