From: Lachnitt <lachnitt@stanford.edu>
Date: Mon, 28 Mar 2022 19:05:26 +0000 (-0700)
Subject: [proofs] Alethe: Call Printer (#8408)
X-Git-Tag: cvc5-1.0.0~152
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e3ad186ff419597b49524086d64bc2011246f897;p=cvc5.git

[proofs] Alethe: Call Printer (#8408)

The alethe printer was not called on Master.
---

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)
   {