From 095b2bdf59c8af920512ee25eb89c3635280407b Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 30 Jan 2026 15:26:21 +0000
Subject: [PATCH] code simplifications

---
 src/util/common_msgs.cpp | 14 +++++++-------
 src/util/common_msgs.h   | 14 +++++++-------
 src/util/mpz.cpp         |  9 ---------
 src/util/mpz.h           |  9 +--------
 src/util/rational.cpp    |  2 +-
 5 files changed, 16 insertions(+), 32 deletions(-)

diff --git a/src/util/common_msgs.cpp b/src/util/common_msgs.cpp
index f55591b43..1534bd484 100644
--- a/src/util/common_msgs.cpp
+++ b/src/util/common_msgs.cpp
@@ -18,10 +18,10 @@ Notes:
 --*/
 #include "util/common_msgs.h"
 
-char const * common_msgs::g_canceled_msg   = "canceled";
-char const * common_msgs::g_max_memory_msg = "max. memory exceeded";
-char const * common_msgs::g_max_scopes_msg = "max. scopes exceeded";
-char const * common_msgs::g_max_steps_msg  = "max. steps exceeded";
-char const * common_msgs::g_max_frames_msg = "max. frames exceeded";
-char const * common_msgs::g_no_proofs_msg  = "component does not support proof generation";
-char const * common_msgs::g_max_resource_msg = "max. resource limit exceeded";
+char const common_msgs::g_canceled_msg[]   = "canceled";
+char const common_msgs::g_max_memory_msg[] = "max. memory exceeded";
+char const common_msgs::g_max_scopes_msg[] = "max. scopes exceeded";
+char const common_msgs::g_max_steps_msg[]  = "max. steps exceeded";
+char const common_msgs::g_max_frames_msg[] = "max. frames exceeded";
+char const common_msgs::g_no_proofs_msg[]  = "component does not support proof generation";
+char const common_msgs::g_max_resource_msg[] = "max. resource limit exceeded";
\ No newline at end of file
diff --git a/src/util/common_msgs.h b/src/util/common_msgs.h
index 83434aa55..e13ca7f59 100644
--- a/src/util/common_msgs.h
+++ b/src/util/common_msgs.h
@@ -20,13 +20,13 @@ Notes:
 
 class common_msgs {
 public:
-    static char const * g_canceled_msg;
-    static char const * g_max_memory_msg;
-    static char const * g_max_scopes_msg;
-    static char const * g_max_steps_msg;
-    static char const * g_max_frames_msg;
-    static char const * g_no_proofs_msg;
-    static char const * g_max_resource_msg;
+    static char const g_canceled_msg[];
+    static char const g_max_memory_msg[];
+    static char const g_max_scopes_msg[];
+    static char const g_max_steps_msg[];
+    static char const g_max_frames_msg[];
+    static char const g_no_proofs_msg[];
+    static char const g_max_resource_msg[];
 };
 
 #define Z3_CANCELED_MSG      common_msgs::g_canceled_msg
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index a1b01e041..6ee634a43 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -188,16 +188,12 @@ template<bool SYNCH>
 mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
     SASSERT(capacity >= m_init_cell_capacity);
     mpz_cell * cell;
-#ifdef SINGLE_THREAD
-    cell = reinterpret_cast<mpz_cell*>(m_allocator.allocate(cell_size(capacity)));
-#else
     if (SYNCH) {
         cell = reinterpret_cast<mpz_cell*>(memory::allocate(cell_size(capacity)));
     }
     else {
         cell = reinterpret_cast<mpz_cell*>(m_allocator.allocate(cell_size(capacity)));
     }
-#endif
     cell->m_capacity = capacity;
 
     return cell;
@@ -206,17 +202,12 @@ mpz_cell * mpz_manager<SYNCH>::allocate(unsigned capacity) {
 template<bool SYNCH>
 void mpz_manager<SYNCH>::deallocate(bool is_heap, mpz_cell * ptr) { 
     if (is_heap) {
-
-#ifdef SINGLE_THREAD
-        m_allocator.deallocate(cell_size(ptr->m_capacity), ptr); 
-#else
         if (SYNCH) {
             memory::deallocate(ptr);
         }
         else {
             m_allocator.deallocate(cell_size(ptr->m_capacity), ptr);        
         }
-#endif
     }
 }
 
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 9e7c991f5..fe3c66077 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -152,6 +152,7 @@ class mpz_manager {
     mutable std::recursive_mutex    m_lock;
 #define MPZ_BEGIN_CRITICAL() if (SYNCH) m_lock.lock()
 #define MPZ_END_CRITICAL()   if (SYNCH) m_lock.unlock()
+static_assert(false);
 #else
 #define MPZ_BEGIN_CRITICAL() {}
 #define MPZ_END_CRITICAL()   {}
@@ -211,16 +212,12 @@ class mpz_manager {
 
     mpz_t * allocate() {        
         mpz_t * cell;
-#ifdef SINGLE_THREAD
-        cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));        
-#else
         if (SYNCH) {
             cell = reinterpret_cast<mpz_t*>(memory::allocate(sizeof(mpz_t)));
         }
         else {
             cell = reinterpret_cast<mpz_t*>(m_allocator.allocate(sizeof(mpz_t)));        
         }
-#endif
         mpz_init(*cell);
         return cell;
     }
@@ -228,16 +225,12 @@ class mpz_manager {
     void deallocate(bool is_heap, mpz_t * ptr) { 
         mpz_clear(*ptr); 
         if (is_heap) {
-#ifdef SINGLE_THREAD
-            m_allocator.deallocate(sizeof(mpz_t), ptr); 
-#else
             if (SYNCH) {
                 memory::deallocate(ptr);
             }
             else {
                 m_allocator.deallocate(sizeof(mpz_t), ptr); 
             }
-#endif
         }
     }
 
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
index e11245fa3..c9b2033d1 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational.cpp
@@ -44,8 +44,8 @@ static DECLARE_MUTEX(g_powers_of_two);
 
 rational rational::power_of_two(unsigned k) {
     rational result;
-    lock_guard lock(*g_powers_of_two);
     {
+        lock_guard lock(*g_powers_of_two);
         if (k >= m_powers_of_two.size())
             mk_power_up_to(m_powers_of_two, k+1);
         result = m_powers_of_two[k];