mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

Narrow TPTP parser restoration catches

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

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-23 23:19:22 +00:00 • committed by GitHub
parent aac0a49c5b
commit 69b78bf072
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 19 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/cmd_context/tptp_frontend.cpp
View file

@ -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);