From e50c22099d8adfa0a33d217e1857d3de986e6c05 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 13 May 2026 15:56:14 +0000 Subject: [PATCH] Harden scoped implicit-variable RAII in TPTP frontend Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/38c3a47d-1e93-48d8-8fa4-1dfc724e76e5 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/cmd_context/tptp_frontend.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index f086473e9..671059984 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -414,7 +414,7 @@ class tptp_parser { app* get_or_create_implicit_var(std::string const& n) { if (!m_implicit_scope) - throw parse_error("internal parser error: implicit variable scope is missing"); + throw parse_error("internal parser error: implicit variable scope is missing (unexpected parser state)"); auto it = m_implicit_scope->vars.find(n); if (it != m_implicit_scope->vars.end()) return it->second; app* c = m.mk_const(symbol(n), m_univ); @@ -432,6 +432,10 @@ class tptp_parser { m_prev_scope(p.m_implicit_scope) { m_p.m_implicit_scope = &scope; } + scoped_implicit_vars(scoped_implicit_vars const&) = delete; + scoped_implicit_vars& operator=(scoped_implicit_vars const&) = delete; + scoped_implicit_vars(scoped_implicit_vars&&) = delete; + scoped_implicit_vars& operator=(scoped_implicit_vars&&) = delete; ~scoped_implicit_vars() { m_p.m_implicit_scope = m_prev_scope; }