From 4831c45ad8fcc5796b07faf070e47603b662756e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Feb 2017 13:38:07 -0800
Subject: [PATCH] fix issues in par

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_par.cpp    | 14 +++++++++-----
 src/sat/sat_solver.cpp | 14 +++++++++++---
 2 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/src/sat/sat_par.cpp b/src/sat/sat_par.cpp
index 8b8c8e309..cd8901e09 100644
--- a/src/sat/sat_par.cpp
+++ b/src/sat/sat_par.cpp
@@ -77,9 +77,14 @@ namespace sat {
 
     bool par::vector_pool::get_vector(unsigned owner, unsigned& n, unsigned const*& ptr) {
         unsigned head = m_heads[owner];      
+        unsigned iterations = 0;
         while (head != m_tail) {
+            ++iterations;
+            if (head == 0 && m_tail >= m_size) {
+                break;
+            }
             SASSERT(head < m_size);
-            IF_VERBOSE(3, verbose_stream() << owner << ": head: " << head << " tail: " << m_tail << "\n";);
+            IF_VERBOSE((iterations > m_size ? 0 : 3), verbose_stream() << owner << ": head: " << head << " tail: " << m_tail << "\n";);
             bool is_self = owner == get_owner(head);
             next(m_heads[owner]);
             if (!is_self) {
@@ -88,9 +93,6 @@ namespace sat {
                 return true;
             }
             head = m_heads[owner];
-            if (head == 0 && m_tail >= m_size) {
-                break;
-            }
         }
         return false;
     }
@@ -107,8 +109,10 @@ namespace sat {
         unsigned num_threads = num_extra_solvers + 1;
         m_solvers.resize(num_extra_solvers, 0);
         symbol saved_phase = s.m_params.get_sym("phase", symbol("caching"));
-        for (unsigned i = 0; i < num_extra_solvers; ++i) {
+        for (unsigned i = 0; i < num_extra_solvers; ++i) {        
             m_limits.push_back(reslimit());
+        }
+        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) {
                 s.m_params.set_sym("phase", symbol("random"));
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 2dcbf7cbb..c843fc900 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -364,6 +364,11 @@ namespace sat {
         }
         unsigned some_idx = c.size() >> 1;
         literal block_lit = c[some_idx];
+        if (m_watches.size() <= (~c[0]).index()) std::cout << c << "\n";
+        if (m_watches.size() <= (~c[1]).index()) std::cout << c << "\n";
+        if (m_watches[(~c[0]).index()].size() >= 20000) {
+            std::cout << m_par_id << ": " << c << "\n";
+        }
         m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
         m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
         return reinit;
@@ -836,7 +841,8 @@ namespace sat {
         int num_threads = static_cast<int>(m_config.m_num_parallel);
         int num_extra_solvers = num_threads - 1;
         sat::par par(*this);
-        par.reserve(num_threads, 1 << 16);
+        // par.reserve(num_threads, 1 << 16);
+        par.reserve(num_threads, 1 << 9);
         par.init_solvers(*this, num_extra_solvers);
         int finished_id = -1;
         std::string        ex_msg;
@@ -877,8 +883,10 @@ namespace sat {
                         }
                     }
                     if (i != num_extra_solvers) {
-                        canceled = rlimit().inc();
-                        rlimit().cancel();
+                        canceled = !rlimit().inc();
+                        if (!canceled) {
+                            rlimit().cancel();
+                        }
                     }
                 }                
             }