mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

incorrect offset calculation in diff logic optimization. codeplex issue 156

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-12-29 16:15:19 -08:00
parent 7d62ceeadc
commit a296023823
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_diff_logic_def.h
View file

@ -1237,7 +1237,7 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
}
}
blocker = mk_gt(v, r);
return inf_eps(rational(0), r);
return inf_eps(rational(0), r + m_objective_consts[v]);
}
default:
TRACE("opt", tout << "unbounded\n"; );
@ -1295,7 +1295,7 @@ expr_ref theory_diff_logic<Ext>::block_objective(theory_var v, inf_rational cons
return f;
}
inf_rational new_val = val - inf_rational(m_objective_consts[v]);
inf_rational new_val = val; // - inf_rational(m_objective_consts[v]);
e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));
if (new_val.get_infinitesimal().is_neg()) {