squash-merge from proof branch

1 files changed, 19 insertions, 8 deletions

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 63a09169f..268a90cf6 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -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;
         }