mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-13 17:41:16 +00:00
Code Activity

fixup comparison with bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-30 08:26:13 -07:00
parent 6ba4ba142f
commit 706aff74ff
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/nla_bounds.cpp
View file

@ -57,6 +57,13 @@ namespace nla {
return false; return false;
if (c().var_is_fixed(j)) if (c().var_is_fixed(j))
return false; return false;
u_dependency *d = nullptr;
lp::mpq bound;
bool is_strict;
if (c().has_lower_bound(j, d, bound, is_strict) && (bound > value || (bound == value && is_strict)))
return false;
if (c().has_upper_bound(j, d, bound, is_strict) && (bound < value || (bound == value && is_strict)))
return false;
// fix a bound that hasn't already been fixed. // fix a bound that hasn't already been fixed.
if (c().has_lower_bound(j) && c().get_lower_bound(j) == value) { if (c().has_lower_bound(j) && c().get_lower_bound(j) == value) {
auto i(ineq(j, lp::lconstraint_kind::LE, rational(value))); auto i(ineq(j, lp::lconstraint_kind::LE, rational(value)));