mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix #2945

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-09 15:43:21 -08:00
parent 1eb4459325
commit 82273da630
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/opt/opt_solver.cpp
View file

@ -186,6 +186,9 @@ namespace opt {
r = m_context.check(num_assumptions, assumptions);
}
r = adjust_result(r);
if (r == l_true) {
m_context.get_model(m_model);
}
m_first = false;
if (dump_benchmarks()) {
w.stop();

9
src/opt/optsmt.cpp
View file

@ -114,7 +114,7 @@ namespace opt {
SASSERT(delta_per_step.is_int());
SASSERT(delta_per_step.is_pos());
is_sat = m_s->check_sat(0, nullptr);
if (is_sat == l_true) {
if (is_sat == l_true) {
bound = update_lower();
if (!get_max_delta(lower, delta_index)) {
delta_per_step = rational::one();
@ -176,12 +176,11 @@ namespace opt {
arith_util arith(m);
bool is_int = arith.is_int(m_objs[obj_index].get());
lbool is_sat = l_true;
expr_ref bound(m);
expr_ref bound(m), last_bound(m);
for (unsigned i = 0; i < obj_index; ++i) {
commit_assignment(i);
}
m_s->get_model(m_model);
unsigned steps = 0;
unsigned step_incs = 0;
@ -219,7 +218,11 @@ namespace opt {
bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
}
TRACE("opt", tout << "delta: " << delta_per_step << " " << bound << "\n";);
if (bound == last_bound) {
break;
}
m_s->assert_expr(bound);
last_bound = bound;
}
else if (is_sat == l_false && delta_per_step > rational::one()) {
steps = 0;