From a296023823fbb94da7a80307edc96b326fe271dd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Dec 2014 16:15:19 -0800 Subject: [PATCH] incorrect offset calculation in diff logic optimization. codeplex issue 156 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_diff_logic_def.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 3b9993074..ee9823912 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1237,7 +1237,7 @@ theory_diff_logic::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::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()) {