1 files changed, 25 insertions, 14 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 63a09169f..4a4515eb9 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -1,13 +1,13 @@
 /*********************                                                        */
 /*! \file theory_proxy.cpp
  ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett, Christopher L. Conway, Tim King, Liana Hadarean
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
  **
  ** \brief [[ Add one-line brief description here ]]
  **
@@ -98,19 +98,30 @@ void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
 void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
-  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
-  PROOF(ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); );
-  Debug("prop-explain") << "explainPropagation() => " <<  theoryExplanation << std::endl;
-  if (theoryExplanation.getKind() == kind::AND) {
-    Node::const_iterator it = theoryExplanation.begin();
-    Node::const_iterator it_end = theoryExplanation.end();
+
+  NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode);
+  Node explanationNode = theoryExplanation.node;
+  theory::TheoryId explainerTheory = theoryExplanation.theory;
+
+  PROOF({
+      ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode);
+      ProofManager::getCnfProof()->setExplainerTheory(explainerTheory);
+
+      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: "
+                        << explainerTheory << std::endl;
+    });
+
+  Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl;
+  if (explanationNode.getKind() == kind::AND) {
+    Node::const_iterator it = explanationNode.begin();
+    Node::const_iterator it_end = explanationNode.end();
     explanation.push_back(l);
     for (; it != it_end; ++ it) {
       explanation.push_back(~d_cnfStream->getLiteral(*it));
     }
   } else {
     explanation.push_back(l);
-    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
+    explanation.push_back(~d_cnfStream->getLiteral(explanationNode));
   }
 }
 
@@ -164,7 +175,7 @@ void TheoryProxy::notifyRestart() {
           if(lemmaCount % 1 == 0) {
             Debug("shared") << "=) " << asNode << std::endl;
           }
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }