Fixing a case for explanation of non-normal form equalities.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 2c863ba841b08b461e40e1ff0c1ab36b90be30b4..eb0c99abe4d481be4d312585acf33b59776cf349 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1723,9 +1723,16 @@ Node TheoryArith::explain(TNode n) {
     return exp;
   }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
     c = d_assertionsThatDoNotMatchTheirLiterals[n];
-    Node exp = c->explainForPropagation();
-    Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
-    return exp;
+    if(!c->isSelfExplaining()){
+      Node exp = c->explainForPropagation();
+      Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
+      return exp;
+    }else{
+      Debug("arith::explain") << "this is a strange mismatch" << n << endl;
+      Assert(d_congruenceManager.canExplain(n));
+      Debug("arith::explain") << "this is a strange mismatch" << n << endl;
+      return d_congruenceManager.explain(n);
+    }
   }else{
     Assert(d_congruenceManager.canExplain(n));
     Debug("arith::explain") << "dm explanation" << n << endl;