From 97193b4a1d623a4c6cd57c0fde779a77b2061ae1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Jul 2025 14:15:15 -0700 Subject: [PATCH] call into collect_statistics in case of -T interrupt --- src/solver/tactic2solver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 09568f330..618d9c161 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -309,6 +309,8 @@ solver* tactic2solver::translate(ast_manager& m, params_ref const& p) { void tactic2solver::collect_statistics(statistics & st) const { st.copy(m_stats); + if (m_stats.size() == 0 && m_tactic) + m_tactic->collect_statistics(st); //SASSERT(m_stats.size() > 0); }