fix model return after shutdown, reported in #4532

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Jul 28, 2020 · 8857a67 · 8857a67
1 parent b71a643
commit 8857a67
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 2 deletions.
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
@@ -4486,8 +4486,12 @@ namespace smt {
     }
 
     void context::get_model(model_ref & mdl) {
-        if (inconsistent() || !m.inc())
-            mdl = nullptr;       
+        if (inconsistent()) 
+            mdl = nullptr;
+        else if (m_model.get()) 
+            mdl = m_model.get();
+        else if (!m.inc())
+            mdl = nullptr;
         else {
             mk_proto_model();
             if (!m_model && m_proto_model) {

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
@@ -162,6 +162,7 @@ namespace smt {
                     pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
                     return;
                 } 
+
 
                 bool first = false;
                 {

diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
@@ -433,6 +433,9 @@ class parallel_tactic : public tactic {
             }
             m_models.push_back(mdl.get());
         }
+        else if (m_models.empty()) {
+            m_has_undef = true;
+        }
         if (!m_allsat) {
             m_queue.shutdown();
         }
-Original file line number
+Diff line change
@@ Expand Up / @@ -162,6 +162,7 @@ namespace smt { @@
                         pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
                         return;
                     }
                     bool first = false;
                     {
@@ Expand Down @@