From 8744c62fca91dddc0c88786c8646f716e53e6e45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Jul 2018 10:55:25 +0100 Subject: [PATCH] fix #1755 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index ca0474314..e61a02d80 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -230,11 +230,14 @@ namespace opt { get_model(m_model); inf_eps val2; m_valid_objectives[i] = true; - TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";); + TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << "\n";); if (!m_models[i]) { set_model(i); } - if (m_context.get_context().update_model(has_shared)) { + if (!val.is_finite()) { + // skip model updates + } + else if (m_context.get_context().update_model(has_shared)) { if (has_shared && val != current_objective_value(i)) { decrement_value(i, val); }