From 256a0e2d8291b722bf286a828f481f98d28fe568 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Feb 2017 12:12:26 -0800
Subject: [PATCH] move exchange par

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp | 9 ++++-----
 src/sat/sat_solver.h   | 1 +
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index fff9ee6e4..376b4f8d5 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -84,7 +84,7 @@ namespace sat {
                 VERIFY(v == mk_var(ext, dvar));
             }
         }
-        unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
+        unsigned sz = src.init_trail_size();
         for (unsigned i = 0; i < sz; ++i) {
             assign(src.m_trail[i], justification());
         }
@@ -774,7 +774,6 @@ namespace sat {
 
                 restart();
                 simplify_problem();
-                exchange_par();
                 if (check_inconsistent()) return l_false;
                 gc();
 
@@ -890,9 +889,8 @@ namespace sat {
      */
     void solver::exchange_par() {
         if (m_par && scope_lvl() == 0) {
-            unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
+            unsigned sz = init_trail_size();
             unsigned num_in = 0, num_out = 0;
-            SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
             literal_vector in, out;
             for (unsigned i = m_par_limit_out; i < sz; ++i) {
                 literal lit = m_trail[i];
@@ -2546,6 +2544,7 @@ namespace sat {
 
     void solver::pop_reinit(unsigned num_scopes) {
         pop(num_scopes);
+        exchange_par();
         reinit_assumptions();
     }
 
@@ -2865,7 +2864,7 @@ namespace sat {
     }
 
     void solver::display_units(std::ostream & out) const {
-        unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
+        unsigned end = init_trail_size();
         for (unsigned i = 0; i < end; i++) {
             out << m_trail[i] << " ";
         }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 54b8a9bb2..f910e374f 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -223,6 +223,7 @@ namespace sat {
         lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
         unsigned lvl(bool_var v) const { return m_level[v]; }
         unsigned lvl(literal l) const { return m_level[l.var()]; }
+        unsigned init_trail_size() const { return scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; }
         void assign(literal l, justification j) {
             TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
             switch (value(l)) {