From e3481654f8181e0e28fc53731d8ea5adb631f205 Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 16 Feb 2024 18:08:38 -0300
Subject: [PATCH] remove hack

---
 src/smt/proof_manager.cpp | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 3b75755bfb5..a6734954f56 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -275,12 +275,7 @@ void PfManager::printProof(std::ostream& out,
     vpfpp.process(fp);
     // print using ALF printer
     proof::AlfPrinter alfp(d_env, anc);
-    // Add empty scope since definitions are flattened
-    // TODO: eliminate this by ensuring that the AletheProofPostprocess
-    // preserves the outermost 2 SCOPE.
-    std::vector<Node> emptyAssumps;
-    std::shared_ptr<ProofNode> fps = d_pnm->mkScope(fp, emptyAssumps, false);
-    alfp.print(out, fps);
+    alfp.print(out, fp);
   }
   else if (mode == options::ProofFormatMode::ALETHE)
   {