mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix constant offset and handling of ite in difference logic optimizer code-path. Issue #946

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-24 02:23:50 -07:00
parent 5d11a1cdb2
commit ec47706226
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_dense_diff_logic_def.h
View file

@ -868,7 +868,8 @@ namespace smt {
e = ctx.get_enode(to_app(n));
}
else {
e = ctx.mk_enode(to_app(n), false, false, true);
ctx.internalize(n, false);
e = ctx.get_enode(n);
}
v = e->get_th_var(get_id());
if (v == null_theory_var) {
@ -1008,7 +1009,8 @@ namespace smt {
inf_eps result(rational(0), r);
blocker = mk_gt(v, result);
IF_VERBOSE(10, verbose_stream() << blocker << "\n";);
return result;
r += m_objective_consts[v];
return inf_eps(rational(0), r);
}
default:
TRACE("opt", tout << "unbounded\n"; );