1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 2dbb2a873..71c75ceae 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -16,6 +16,8 @@
 
 #include <iostream>
 
+#include "options/proof_options.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -24,6 +26,7 @@ ProofNodeToSExpr::ProofNodeToSExpr()
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<TypeNode> types;
+  d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->mkSExprType(types));
   d_argsMarker = nm->mkBoundVar(":args", nm->mkSExprType(types));
 }
 
@@ -67,6 +70,11 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn)
       std::vector<Node> children;
       // add proof rule
       children.push_back(getOrMkPfRuleVariable(cur->getRule()));
+      if (options::proofPrintConclusion())
+      {
+        children.push_back(d_conclusionMarker);
+        children.push_back(cur->getResult());
+      }
       const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren();
       for (const std::shared_ptr<ProofNode>& cp : pc)
       {