mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 14:32:06 +00:00
Code Activity

Fix assertion violation in lp_bound_propagator when column has non-zero delta

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-08-07 06:40:54 +00:00 • committed by GitHub
parent 56d5f4ea6d
commit 553f19ca05
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/lp_bound_propagator.h
View file

@ -74,7 +74,7 @@ private:
m_val2fixed_row.insert(val(v1), r1);
return;
}
if (!only_one_nfixed(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) {
if (!only_one_nfixed(r2, v2) || ival(v1) != ival(v2) || is_int(v1) != is_int(v2)) {
m_val2fixed_row.insert(val(v1), r1);
return;
}
@ -331,6 +331,12 @@ public:
if (column_is_fixed(v_j)) {
return;
}
// the columns registered in the fixed tables have a zero infinitesimal part,
// so v_j cannot be equal to any of them when its delta part is not zero
if (!ival(v_j).y.is_zero()) {
try_add_equation_with_internal_fixed_tables(row_index);
return;
}
unsigned j = null_lpvar;
if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
try_add_equation_with_internal_fixed_tables(row_index);