diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4d71172d1..9127c5af9 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2309,15 +2309,22 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) { void cmd_context::flush_statistics() { // Force aggregation of theory statistics before displaying them // This ensures detailed theory stats are available even on timeout/interruption + std::cout << "[DEBUG] cmd_context::flush_statistics() called\n"; if (m_check_sat_result) { + std::cout << "[DEBUG] Calling m_check_sat_result->flush_statistics()\n"; m_check_sat_result->flush_statistics(); } else if (m_solver) { + std::cout << "[DEBUG] Calling m_solver->flush_statistics()\n"; m_solver->flush_statistics(); } else if (m_opt) { + std::cout << "[DEBUG] m_opt exists but flush_statistics not implemented\n"; // m_opt->flush_statistics(); // Not implemented for optimization } + else { + std::cout << "[DEBUG] No solver object found!\n"; + } } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index cfcf541a0..c1b944286 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -148,6 +148,7 @@ namespace { void flush_statistics() override { // Force aggregation of theory statistics before collecting them + std::cout << "[DEBUG] smt_solver::flush_statistics() called\n"; m_context.flush_statistics(); }