declare m_global_stats as std::unique_ptr

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/cmd_context/cmd_context.cpp

@@ -609,6 +609,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_own_manager(m == nullptr),
     m_regular("stdout", std::cout),
     m_diagnostic("stderr", std::cerr),
+    m_global_stats(std::make_unique<statistics>()),
     m_stats_collected(false) {
     SASSERT(m != 0 || !has_manager());
     install_basic_cmds(*this);
@@ -2291,22 +2292,29 @@ void cmd_context::set_solver_factory(solver_factory * f) {
 }
 
 void cmd_context::display_statistics(bool show_total_time, double total_time) {
+    lock_guard lock(m_stats_mutex);
+    
     // If statistics haven't been collected yet, collect them now
     if (!m_stats_collected) {
-        flush_statistics();
+        flush_statistics_unlocked();  // Call unlocked version since we already have the lock
     }
     
     // Add time and memory statistics
     if (show_total_time)
-        m_global_stats.update("total time", total_time);
+        m_global_stats->update("total time", total_time);
-    m_global_stats.update("time", get_seconds());
+    m_global_stats->update("time", get_seconds());
-    get_memory_statistics(m_global_stats);
+    get_memory_statistics(*m_global_stats);
-    get_rlimit_statistics(m().limit(), m_global_stats);
+    get_rlimit_statistics(m().limit(), *m_global_stats);
     
-    m_global_stats.display_smt2(regular_stream());
+    m_global_stats->display_smt2(regular_stream());
 }
 
 void cmd_context::flush_statistics() {
+    lock_guard lock(m_stats_mutex);
+    flush_statistics_unlocked();
+}
+
+void cmd_context::flush_statistics_unlocked() {
     // Only collect statistics once to avoid duplication
     if (m_stats_collected) {
         return;
@@ -2323,7 +2331,7 @@ void cmd_context::flush_statistics() {
         m_check_sat_result->flush_statistics();
         
         // Also collect the statistics immediately into our singleton
-        m_check_sat_result->collect_statistics(m_global_stats);
+        m_check_sat_result->collect_statistics(*m_global_stats);
         collected_from_check_sat = true;
     }
     
@@ -2332,7 +2340,7 @@ void cmd_context::flush_statistics() {
         m_solver->flush_statistics();
         
         // Also collect the statistics immediately into our singleton
-        m_solver->collect_statistics(m_global_stats);
+        m_solver->collect_statistics(*m_global_stats);
     }
     
     // Try to get access to any other solver contexts
@@ -2340,16 +2348,18 @@ void cmd_context::flush_statistics() {
         // m_opt->flush_statistics(); // Not implemented for optimization
         
         // But we can still collect stats
-        m_opt->collect_statistics(m_global_stats);
+        m_opt->collect_statistics(*m_global_stats);
     }
     
     m_stats_collected = true;
 }
 
 void cmd_context::collect_smt_statistics(smt::context& smt_ctx) {
+    lock_guard lock(m_stats_mutex);
+    
     // Collect statistics from SMT context directly into our singleton
     // Collect from the SMT context which should have aggregated theory stats
-    smt_ctx.collect_statistics(m_global_stats);
+    smt_ctx.collect_statistics(*m_global_stats);
     
     m_stats_collected = true;
 }

src/cmd_context/cmd_context.h

@@ -23,6 +23,7 @@ Notes:
 #include<sstream>
 #include<vector>
 #include "util/stopwatch.h"
+#include "util/mutex.h"
 #include "util/stats.h"
 #include "util/cmd_context_types.h"
 #include "util/event_handler.h"
@@ -309,8 +310,10 @@ protected:
     
     // Singleton statistics object to accumulate stats throughout the run
     // This ensures theory statistics collected during timeout are preserved
-    statistics                   m_global_stats;
+    // Using a pointer to avoid any accidental copying
+    std::unique_ptr<statistics>      m_global_stats;
     bool                         m_stats_collected;
+    mutex                        m_stats_mutex;  // Protect statistics access
 
     class dt_eh : public new_datatype_eh {
         cmd_context &             m_owner;
@@ -518,6 +521,7 @@ public:
     void display_assertions();
     void display_statistics(bool show_total_time = false, double total_time = 0.0);
     void flush_statistics();  // Force aggregation of theory statistics
+    void flush_statistics_unlocked();  // Internal helper, requires m_stats_mutex to be held
     void collect_smt_statistics(smt::context& smt_ctx);  // Collect stats from SMT context into singleton
     void display_dimacs();
     void display_parameters(std::ostream& out);

src/smt/smt_context.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "util/warning.h"
 #include "util/timeit.h"
 #include "util/union_find.h"
+#include "util/mutex.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_smt2_pp.h"
@@ -50,7 +51,9 @@ Revision History:
 namespace smt {
 
     // Global pointer to current SMT context for timeout statistics collection
+    // Protected by mutex for thread safety
     static context* g_smt_context = nullptr;
+    static mutex g_smt_context_mutex;
 
     context::context(ast_manager & m, smt_params & p, params_ref const & _p):
         m(m),
@@ -102,8 +105,11 @@ namespace smt {
 
         m_model_generator->set_context(this);
         
-        // Register this SMT context for timeout statistics collection
+        // Register this SMT context for timeout statistics collection (thread-safe)
-        g_smt_context = this;
+        {
+            lock_guard lock(g_smt_context_mutex);
+            g_smt_context = this;
+        }
     }
 
     /**
@@ -195,9 +201,12 @@ namespace smt {
     }
 
     context::~context() {
-        // Unregister this SMT context
+        // Unregister this SMT context (thread-safe)
-        if (g_smt_context == this) {
+        {
-            g_smt_context = nullptr;
+            lock_guard lock(g_smt_context_mutex);
+            if (g_smt_context == this) {
+                g_smt_context = nullptr;
+            }
         }
         flush();
         m_asserted_formulas.finalize();
@@ -4820,6 +4829,7 @@ namespace smt {
     }
     // Function to get the current global SMT context (for timeout handling)
     context* get_current_smt_context() {
+        lock_guard lock(g_smt_context_mutex);
         return g_smt_context;
     }