remove hack

HanielB · Feb 16, 2024 · e348165 · e348165
1 parent e593dff
commit e348165
Showing 1 changed file with 1 addition and 6 deletions.
diff --git 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)
   {