mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 01:46:15 +00:00
Code Activity

fix #3320

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 13:22:17 -07:00
parent daadc1dd8c
commit b3e1e302f7
2 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/maxlex.cpp
View file

@ -82,7 +82,7 @@ namespace opt {
if (first_undef && soft.value != l_undef) { if (first_undef && soft.value != l_undef) {
continue; continue;
} }
if (first_undef) { else if (first_undef) {
SASSERT(soft.value == l_undef); SASSERT(soft.value == l_undef);
soft.set_value(l_true); soft.set_value(l_true);
assert_value(soft); assert_value(soft);

12
src/opt/opt_solver.cpp
View file

@ -292,7 +292,7 @@ namespace opt {
TRACE("opt", tout << is_sat << "\n";); TRACE("opt", tout << is_sat << "\n";);
if (is_sat != l_true) { if (is_sat != l_true) {
// cop-out approximation // cop-out approximation
if (arith_util(m).is_real(m_objective_terms[i].get())) { if (arith_util(m).is_real(m_objective_terms.get(i))) {
val -= inf_eps(inf_rational(rational(0), true)); val -= inf_eps(inf_rational(rational(0), true));
} }
else { else {
@ -382,9 +382,13 @@ namespace opt {
return get_optimizer().value(v); return get_optimizer().value(v);
} }
expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) { expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& _val) {
if (!val.is_finite()) { if (!_val.is_finite()) {
return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m); return expr_ref(_val.is_pos() ? m.mk_false() : m.mk_true(), m);
}
inf_eps val = _val;
if (val.get_infinitesimal().is_neg()) {
val = inf_eps(val.get_rational());
} }
smt::theory_opt& opt = get_optimizer(); smt::theory_opt& opt = get_optimizer();
smt::theory_var v = m_objective_vars[var]; smt::theory_var v = m_objective_vars[var];