mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix a bug in polarity

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-01-10 10:50:56 -10:00
parent 75005d9077
commit 2ca1187b3a
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/gomory.cpp
View file

@ -276,10 +276,12 @@ public:
} }
if (is_real(j)) if (is_real(j))
real_case_in_gomory_cut(- p.coeff(), j); real_case_in_gomory_cut(- p.coeff(), j);
else if (!p.coeff().is_int()) { else {
m_fj = fractional_part(-p.coeff()); if (!p.coeff().is_int()) {
m_one_minus_fj = 1 - m_fj; m_fj = fractional_part(-p.coeff());
int_case_in_gomory_cut(j); m_one_minus_fj = 1 - m_fj;
int_case_in_gomory_cut(j);
}
if (p.coeff().is_pos()) { if (p.coeff().is_pos()) {
if (at_lower(j)) if (at_lower(j))
set_polarity(1); set_polarity(1);