From 428d0b4b668ad800e150d2269a6b693a19a20484 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 10 May 2026 15:23:04 +0000 Subject: [PATCH] Refine TPTP frontend ownership and stream restoration semantics 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 | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/shell/tptp_frontend.cpp b/src/shell/tptp_frontend.cpp index 490f6e3cb..5193c0088 100644 --- a/src/shell/tptp_frontend.cpp +++ b/src/shell/tptp_frontend.cpp @@ -60,9 +60,10 @@ struct parse_error : public std::exception { class scoped_regular_stream { cmd_context& m_ctx; + std::string m_prev; 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"); } + scoped_regular_stream(cmd_context& ctx, std::ostream& out): m_ctx(ctx), m_prev(ctx.get_regular_stream_name()) { m_ctx.set_regular_stream(out); } + ~scoped_regular_stream() { m_ctx.set_regular_stream(m_prev.c_str()); } }; struct token { @@ -374,10 +375,10 @@ class tptp_parser { return false; } - expr_ref mk_quantifier(bool is_forall, ptr_vector const& bound, expr* body) { + expr_ref mk_quantifier(bool is_forall, ptr_vector const& bound, expr_ref const& body) { SASSERT(body); - if (bound.empty()) return expr_ref(body, m); - return is_forall ? ::mk_forall(m, bound.size(), bound.data(), body) : ::mk_exists(m, bound.size(), bound.data(), body); + if (bound.empty()) return body; + return is_forall ? ::mk_forall(m, bound.size(), bound.data(), body.get()) : ::mk_exists(m, bound.size(), bound.data(), body.get()); } parsed_type parse_type_atom() { @@ -767,7 +768,7 @@ expr_ref tptp_parser::parse_term() { expr_ref_vector args(m); for (unsigned i = 0; i < a->get_num_args(); ++i) args.push_back(a->get_arg(i)); args.push_back(arg); - e = m.mk_app(d, args.size(), args.data()); + e = expr_ref(m.mk_app(d, args.size(), args.data()), m); } return e; }