From 8857a67e4f15607f0dc6f2311d62dae48ab55ec5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jul 2020 23:48:19 -0700
Subject: [PATCH] fix model return after shutdown, reported in #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 8 ++++++--
src/smt/smt_parallel.cpp | 1 +
src/solver/parallel_tactic.cpp | 3 +++
3 files changed, 10 insertions(+), 2 deletions(-)
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();
}