From 69b78bf072d49a72fedd546abba3315615c66599 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 23 May 2026 23:19:22 +0000
Subject: [PATCH] Narrow TPTP parser restoration catches

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/ca1df142-d992-4e45-a8b3-859fa70a5222

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/cmd_context/tptp_frontend.cpp | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index cfe6698cf..3d771fce5 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -1693,7 +1693,8 @@ class tptp_parser {
             }
             catch (z3_exception const& ex) {
                 std::ostringstream out;
-                out << "semantic error in formula '" << formula_name << "': " << ex.what();
+                out << "semantic error in formula '" << formula_name << "': " << ex.what()
+                    << "; check the formula body and any related type declarations";
                 throw parse_error(out.str());
             }
         }
@@ -1964,7 +1965,23 @@ public:
         try {
             parse_toplevel(current_file);
         }
-        catch (...) {
+        catch (parse_error const&) {
+            if (pushed_filter)
+                m_name_filters.pop_back();
+            m_input = std::move(saved_input);
+            m_lex = std::move(saved_lex);
+            m_curr = saved_curr;
+            throw;
+        }
+        catch (z3_error const&) {
+            if (pushed_filter)
+                m_name_filters.pop_back();
+            m_input = std::move(saved_input);
+            m_lex = std::move(saved_lex);
+            m_curr = saved_curr;
+            throw;
+        }
+        catch (z3_exception const&) {
             if (pushed_filter)
                 m_name_filters.pop_back();
             m_input = std::move(saved_input);