Partial fix to TheoryEngine::getExplanation so that SharedAssertions request explanat...

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0a9670678083c9f0e9d2ccad6a08246f68489d94..f69fdddcbd917471bc3ab348cd09294dd8703e51 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -630,16 +630,26 @@ Node TheoryEngine::getExplanation(TNode node)
   Node explanation;
 
   // The theory that has explaining to do
-  Theory* theory = theoryOf(atom);
+  Theory* theory;
+
+  //This is true if atom is a shared assertion
+  bool sharedAssertion = false;
+
+  SharedAssertionsMap::iterator find;
+  // "find" will have a value when sharedAssertion is true
   if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) {
-    SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
-    if (find == d_sharedAssertions.end()) {
-      theory = theoryOf(atom);
-    }
+    find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
+    sharedAssertion = (find != d_sharedAssertions.end());
   }
 
   // Get the explanation
-  explanation = theory->explain(node);
+  if(sharedAssertion){
+    theory = theoryOf((*find).second.theory);
+    explanation = theory->explain((*find).second.node);
+  } else {
+    theory = theoryOf(atom);
+    explanation = theory->explain(node);
+  }
 
   // Explain any shared equalities that might be in the explanation
   if (d_sharedTermsExist) {