Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

1 files changed, 5 insertions, 15 deletions

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 41da4546e..d0ba4ca71 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -76,22 +76,12 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  LemmaProofRecipe* proofRecipe = NULL;
-  PROOF(proofRecipe = new LemmaProofRecipe;);
+  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
 
-  Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
-
-  PROOF({
-      ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
-      ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
-
-      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
-                       << std::endl;
-      proofRecipe->dump("pf::sat");
-
-      delete proofRecipe;
-      proofRecipe = NULL;
-    });
+  if (options::unsatCores())
+  {
+    ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
+  }
 
   Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
   if (theoryExplanation.getKind() == kind::AND) {