From 0e651eee0457b525677ed3a23bbc1df353122ff8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 28 Oct 2022 14:12:28 -0700
Subject: [PATCH] #6421
---
src/opt/opt_solver.cpp | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 64bf389bf..ee91b06a4 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -287,7 +287,9 @@ namespace opt {
bool ok = bound_value(i, val);
if (l_true != m_context.check(0, nullptr))
return false;
- m_context.get_model(m_last_model);
+ m_context.get_model(m_last_model);
+ if (!m_last_model)
+ return false;
update_objective();
return ok;
};
@@ -299,7 +301,9 @@ namespace opt {
TRACE("opt", tout << "updated\n";);
m_last_model = nullptr;
m_context.get_model(m_last_model);
- if (!has_shared || val == current_objective_value(i))
+ if (!m_last_model)
+ return false;
+ else if (!has_shared || val == current_objective_value(i))
m_models.set(i, m_last_model.get());
else if (!check_bound())
return false;