From d9a48ae91dccf198ca67ecf4c803cc8821937e04 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 May 2026 01:16:14 -0700 Subject: [PATCH] fix timeout event handler Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tptp_frontend.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index d87d01754..9f95f9712 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -17,11 +17,18 @@ #include "solver/solver.h" #include "util/error_codes.h" #include "util/rational.h" +#include "util/timeout.h" #include "util/z3_exception.h" bool g_display_statistics = false; bool g_display_model = false; +static void on_timeout() { + std::cout << "% SZS status Timeout\n"; + std::cout.flush(); + _Exit(0); +} + namespace { enum class token_kind { @@ -1497,6 +1504,7 @@ expr_ref tptp_parser::parse_formula() { } static unsigned read_tptp_stream(std::istream& in, char const* current_file) { + register_on_timeout_proc(on_timeout); try { cmd_context ctx; ctx.set_solver_factory(mk_smt_strategic_solver_factory());