mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

t1

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-30 14:36:14 -07:00
parent fd4cc17689
commit 6712b769a6
2 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/cmd_context/cmd_context.cpp
View file

@ -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";
}
}

1
src/smt/smt_solver.cpp
View file

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