diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 5a620c232..5a418e38d 100644
--- 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
index 591137b9a..dbd9ab834 100644
--- 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
index ec3e50a83..5ec1e908b 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -433,6 +433,9 @@ private:
             }
             m_models.push_back(mdl.get());
         }
+        else if (m_models.empty()) {
+            m_has_undef = true;
+        }
         if (!m_allsat) {
             m_queue.shutdown();
         }