From 9adfeedc9ffa7a8d3aa9edeeefe48e572eacb0dd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 10 May 2026 15:20:28 +0000 Subject: [PATCH] Make TPTP check-sat stream redirection exception-safe Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/2a6b01d0-c799-4e44-aa73-ef228cb4402e Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/shell/tptp_frontend.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/shell/tptp_frontend.cpp b/src/shell/tptp_frontend.cpp index 44b52770f..b7ef07c65 100644 --- a/src/shell/tptp_frontend.cpp +++ b/src/shell/tptp_frontend.cpp @@ -58,6 +58,13 @@ struct parse_error : public std::exception { char const* what() const noexcept override { return m_msg.c_str(); } }; +class scoped_regular_stream { + cmd_context& m_ctx; +public: + scoped_regular_stream(cmd_context& ctx, std::ostream& out): m_ctx(ctx) { m_ctx.set_regular_stream(out); } + ~scoped_regular_stream() { m_ctx.set_regular_stream("stdout"); } +}; + struct token { token_kind kind = token_kind::eof_tok; std::string text; @@ -788,9 +795,8 @@ unsigned read_tptp(char const* file_name) { else p.parse_stream(std::cin); std::ostringstream sink; - ctx.set_regular_stream(sink); + scoped_regular_stream scoped_stream(ctx, sink); ctx.check_sat(0, nullptr); - ctx.set_regular_stream("stdout"); switch (ctx.cs_state()) { case cmd_context::css_unsat: if (p.has_conjecture()) std::cout << "% SZS status Theorem\n";