1 files changed, 26 insertions, 12 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index d0d593f8a..1b9e78d80 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -75,26 +75,40 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  theory::TrustNode texp = d_theoryEngine->getExplanation(lNode);
-  Node theoryExplanation = texp.getNode();
-
+  theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
+  Node theoryExplanation = tte.getNode();
+  if (CVC4::options::proofNew())
+  {
+    d_propEngine->getProofCnfStream()->convertPropagation(tte);
+  }
   if (options::unsatCores())
   {
     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();
-    explanation.push_back(l);
-    for (; it != it_end; ++ it) {
-      explanation.push_back(~d_cnfStream->getLiteral(*it));
+  explanation.push_back(l);
+  if (theoryExplanation.getKind() == kind::AND)
+  {
+    for (const Node& n : theoryExplanation)
+    {
+      explanation.push_back(~d_cnfStream->getLiteral(n));
     }
-  } else {
-    explanation.push_back(l);
+  }
+  else
+  {
     explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
   }
+  if (Trace.isOn("sat-proof"))
+  {
+    std::stringstream ss;
+    ss << "TheoryProxy::explainPropagation: clause for lit is ";
+    for (unsigned i = 0, size = explanation.size(); i < size; ++i)
+    {
+      ss << explanation[i] << " [" << d_cnfStream->getNode(explanation[i])
+         << "] ";
+    }
+    Trace("sat-proof") << ss.str() << "\n";
+  }
 }
 
 void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {