From e3ad186ff419597b49524086d64bc2011246f897 Mon Sep 17 00:00:00 2001
From: Lachnitt <lachnitt@stanford.edu>
Date: Mon, 28 Mar 2022 12:05:26 -0700
Subject: [PATCH] [proofs] Alethe: Call Printer (#8408)

The alethe printer was not called on Master.
---
 src/smt/proof_manager.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 7858769ea..a4278b55a 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -21,6 +21,7 @@
 #include "options/smt_options.h"
 #include "proof/alethe/alethe_node_converter.h"
 #include "proof/alethe/alethe_post_processor.h"
+#include "proof/alethe/alethe_printer.h"
 #include "proof/dot/dot_printer.h"
 #include "proof/lfsc/lfsc_post_processor.h"
 #include "proof/lfsc/lfsc_printer.h"
@@ -185,6 +186,8 @@ void PfManager::printProof(std::ostream& out,
     proof::AletheNodeConverter anc;
     proof::AletheProofPostprocess vpfpp(d_pnm.get(), anc);
     vpfpp.process(fp);
+    proof::AletheProofPrinter vpp;
+    vpp.print(out, fp);
   }
   else if (options().proof.proofFormatMode == options::ProofFormatMode::LFSC)
   {
-- 
2.30.2