mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix model return after shutdown, reported in #4532
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b71a64365d
commit
8857a67e4f
|
@ -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) {
|
||||
|
|
|
@ -162,6 +162,7 @@ namespace smt {
|
|||
pctx.assert_expr(mk_not(mk_and(pctx.unsat_core())));
|
||||
return;
|
||||
}
|
||||
|
||||
|
||||
bool first = false;
|
||||
{
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue