mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 15:37:58 +00:00
Code Activity

fix the debug build

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-07-01 12:34:02 -07:00
parent 4c62c8a040
commit ac27b4d6a2
3 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/cmd_context.h
View file

@ -311,7 +311,7 @@ protected:
// Singleton statistics object to accumulate stats throughout the run // Singleton statistics object to accumulate stats throughout the run
// This ensures theory statistics collected during timeout are preserved // This ensures theory statistics collected during timeout are preserved
// Using a pointer to avoid any accidental copying // Using a pointer to avoid any accidental copying
std::unique_ptr<statistics> m_global_stats; std::unique_ptr<statistics> m_global_stats;
bool m_stats_collected; bool m_stats_collected;
mutex m_stats_mutex; // Protect statistics access mutex m_stats_mutex; // Protect statistics access

3
src/smt/smt_context_pp.cpp
View file

@ -28,9 +28,8 @@ Revision History:
namespace smt { namespace smt {
void context::flush_statistics() { void context::flush_statistics() {
// Only collect statistics once to avoid duplication // Only collect statistics once to avoid duplication
if (m_statistics_collected) { if (m_statistics_collected)
return; return;
}
// Force aggregation of theory statistics into m_aux_stats // Force aggregation of theory statistics into m_aux_stats
// This ensures that detailed theory statistics are available even on timeout/interruption // This ensures that detailed theory statistics are available even on timeout/interruption

2
src/smt/smt_kernel.cpp
View file

@ -258,7 +258,7 @@ namespace smt {
} }
void kernel::flush_statistics() { void kernel::flush_statistics() {
IF_LOG(DEBUG, log() << "smt::kernel::flush_statistics() called\n";); TRACE(smt_kernel, tout << "smt::kernel::flush_statistics() called\n";);
m_imp->m_kernel.flush_statistics(); m_imp->m_kernel.flush_statistics();
} }