From e8e636c3ec5a63fa0a3e7f3c4d94b943f9b9fccb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Oct 2023 19:24:21 +0900
Subject: [PATCH] fix #6936

---
 src/sat/sat_parallel.cpp | 25 ++++++++-----------------
 src/util/rlimit.h        |  7 ++++---
 2 files changed, 12 insertions(+), 20 deletions(-)

diff --git a/src/sat/sat_parallel.cpp b/src/sat/sat_parallel.cpp
index cdb13706f..9f531d19c 100644
--- a/src/sat/sat_parallel.cpp
+++ b/src/sat/sat_parallel.cpp
@@ -25,12 +25,7 @@ namespace sat {
     void parallel::vector_pool::next(unsigned& index) {
         SASSERT(index < m_size);
         unsigned n = index + 2 + get_length(index);
-        if (n >= m_size) {
-            index = 0;
-        }
-        else {
-            index = n;
-        }
+        index = (n >= m_size) ? 0 : n;
     }
 
     void parallel::vector_pool::reserve(unsigned num_threads, unsigned sz) {
@@ -64,9 +59,8 @@ namespace sat {
     }
 
     void parallel::vector_pool::end_add_vector() {
-        if (m_tail >= m_size) {
+        if (m_tail >= m_size) 
             m_tail = 0;
-        }
     }
 
 
@@ -93,9 +87,9 @@ namespace sat {
     parallel::parallel(solver& s): m_num_clauses(0), m_consumer_ready(false), m_scoped_rlimit(s.rlimit()) {}
 
     parallel::~parallel() {
-        for (unsigned i = 0; i < m_solvers.size(); ++i) {            
-            dealloc(m_solvers[i]);
-        }
+        m_limits.reset();
+        for (auto* s : m_solvers)
+            dealloc(s);
     }
 
     void parallel::init_solvers(solver& s, unsigned num_extra_solvers) {
@@ -106,9 +100,8 @@ namespace sat {
         
         for (unsigned i = 0; i < num_extra_solvers; ++i) {
             s.m_params.set_uint("random_seed", s.m_rand());
-            if (i == 1 + num_threads/2) {
+            if (i == 1 + num_threads/2) 
                 s.m_params.set_sym("phase", symbol("random"));
-            }                        
             m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
             m_solvers[i]->copy(s, true);
             m_solvers[i]->set_par(this, i);
@@ -164,9 +157,8 @@ namespace sat {
         IF_VERBOSE(3, verbose_stream() << owner << ": share " <<  c << "\n";);
         lock_guard lock(m_mux);
         m_pool.begin_add_vector(owner, n);                
-        for (unsigned i = 0; i < n; ++i) {
+        for (unsigned i = 0; i < n; ++i) 
             m_pool.add_vector_elem(c[i].index());
-        }
         m_pool.end_add_vector();        
     }
 
@@ -220,9 +212,8 @@ namespace sat {
         if (m_priorities.empty())
             return;
         
-        for (bool_var v = 0; v < m_priorities.size(); ++v) {
+        for (bool_var v = 0; v < m_priorities.size(); ++v) 
             s.update_activity(v, m_priorities[v]);
-        }
         s.m_activity_inc = 128;
 #endif
     }
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index 9be53cd55..0abb06cb3 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -91,8 +91,9 @@ public:
 
 struct scoped_limits {
     reslimit&  m_limit;
-    unsigned   m_sz;
-    scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {}
-    ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
+    unsigned   m_sz = 0;
+    scoped_limits(reslimit& lim): m_limit(lim) {}    
+    ~scoped_limits() { reset(); }
+    void reset() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); m_sz = 0; }
     void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
 };