mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #7569

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-07 11:52:49 -08:00
parent 54c6b11621
commit c002c77e5a
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/opt/optsmt.cpp
View file

@ -133,9 +133,11 @@ namespace opt {
// only try to improve delta_index. // only try to improve delta_index.
bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step)); bound = m_s->mk_ge(delta_index, m_lower[delta_index] + inf_eps(delta_per_step));
} }
TRACE("opt", tout << "index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";); TRACE("opt", tout << mk_pp(m_objs.get(delta_index), m) << " index: " << delta_index << " delta: " << delta_per_step << " : " << bound << "\n";);
if (bound == last_bound) { if (bound == last_bound) {
is_sat = l_false; is_sat = l_false;
if (!m_lower[delta_index].is_finite() && !m_upper[delta_index].is_finite())
m_lower[delta_index] = m_upper[delta_index];
} }
else { else {
m_s->assert_expr(bound); m_s->assert_expr(bound);
@ -155,7 +157,8 @@ namespace opt {
else if (is_sat == l_false) { else if (is_sat == l_false) {
// we are done with this delta_index. // we are done with this delta_index.
m_upper[delta_index] = m_lower[delta_index]; m_upper[delta_index] = m_lower[delta_index];
if (num_scopes > 0) m_s->pop(num_scopes); if (num_scopes > 0)
m_s->pop(num_scopes);
num_scopes = 0; num_scopes = 0;
last_bound = nullptr; last_bound = nullptr;
bool all_tight = true; bool all_tight = true;