mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

fixing calls, signs

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-08-22 09:29:12 -07:00
parent 818b1129a5
commit e8929041b8
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/lar_solver.cpp
View file

@ -333,12 +333,13 @@ namespace lp {
if (improve_lower_bound) if (improve_lower_bound)
term.negate(); term.negate();
impq bound; impq bound;
if (!maximize_term_on_tableau(term, bound)) if (!maximize_term_on_corrected_r_solver(term, bound))
return false; return false;
return false; return false;
// TODO // TODO
if (improve_lower_bound) { if (improve_lower_bound) {
bound.neg();
if (column_has_lower_bound(j) && bound.x == column_lower_bound(j).x) if (column_has_lower_bound(j) && bound.x == column_lower_bound(j).x)
return false; return false;
SASSERT(!column_has_lower_bound(j) || column_lower_bound(j).x < bound.x); SASSERT(!column_has_lower_bound(j) || column_lower_bound(j).x < bound.x);

2
src/math/lp/nla_core.cpp
View file

@ -1548,7 +1548,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
if (no_effect()) if (no_effect())
m_monomial_bounds(); m_monomial_bounds();
if (l_vec.empty() && !done() && improve_bounds()) if (no_effect() && improve_bounds())
return l_false; return l_false;
{ {