From 945cd3169e10262c4e8c69d682f703fb4f82e3e6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Mar 2020 10:43:52 -0700
Subject: [PATCH] fix #3440

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

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5e274c3ce..d57d85ab0 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1189,7 +1189,8 @@ namespace sat {
             m_cleaner(true);
             return do_local_search(num_lits, lits);
         }
-        if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || m_config.m_ddfw_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) {
+        if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0 || 
+             m_config.m_ddfw_threads > 0 || m_config.m_unit_walk_threads > 0) && !m_par) {
             SASSERT(scope_lvl() == 0);
             return check_par(num_lits, lits);
         }
@@ -1453,17 +1454,17 @@ namespace sat {
             m_stats = par.get_solver(finished_id).m_stats;
         }
         if (result == l_true && IS_AUX_SOLVER(finished_id)) {
-            set_model(par.get_solver(finished_id).get_model());
+            set_model(par.get_solver(finished_id).get_model(), true);
         }
         else if (result == l_false && IS_AUX_SOLVER(finished_id)) {
             m_core.reset();
             m_core.append(par.get_solver(finished_id).get_core());
         }
         if (result == l_true && IS_LOCAL_SEARCH(finished_id)) {
-            set_model(ls[finished_id - local_search_offset]->get_model());
+            set_model(ls[finished_id - local_search_offset]->get_model(), true);
         }
         if (result == l_true && IS_UNIT_WALK(finished_id)) {
-            set_model(uw[finished_id - unit_walk_offset]->get_model());
+            set_model(uw[finished_id - unit_walk_offset]->get_model(), true);
         }
         if (!canceled) {
             rlimit().reset_cancel();
@@ -1963,10 +1964,10 @@ namespace sat {
         }
     }
 
-    void solver::set_model(model const& mdl) {
+    void solver::set_model(model const& mdl, bool is_current) {
         m_model.reset();
         m_model.append(mdl);
-        m_model_is_current = !m_model.empty();
+        m_model_is_current = is_current;
     }
 
     void solver::mk_model() {
@@ -2956,7 +2957,7 @@ namespace sat {
             // apply optional clause minimization by detecting subsumed literals.
             // initial experiment suggests it has no effect.
             m_mus(); // ignore return value on cancelation.
-            set_model(m_mus.get_model());
+            set_model(m_mus.get_model(), !m_mus.get_model().empty());
             IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
         }
     }
@@ -4488,7 +4489,7 @@ namespace sat {
         else {
             is_sat = get_consequences(asms, lits, conseq);
         }
-        set_model(mdl);
+        set_model(mdl, !mdl.empty());
         return is_sat;
     }
 
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index bb0b1cde3..f95b316d4 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -445,7 +445,7 @@ namespace sat {
         literal_vector const& get_core() const override { return m_core; }
         model_converter const & get_model_converter() const { return m_mc; }
         void flush(model_converter& mc) override { mc.flush(m_mc); }
-        void set_model(model const& mdl);
+        void set_model(model const& mdl, bool is_current);
         char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); }
         bool check_clauses(model const& m) const;
         bool is_assumption(bool_var v) const;