mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 03:42:04 +00:00
Code Activity

formatting

Browse source
This commit is contained in:
Lev Nachmanson 2025-03-06 14:20:44 -10:00
parent 1ac9c558c0
commit e1cb1bc326
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1902,7 +1902,9 @@ namespace lp {
lia_move r; lia_move r;
do { do {
r = rewrite_eqs(f_vector); r = rewrite_eqs(f_vector);
if (lra.settings().get_cancel_flag()) return lia_move::undef; if (lra.settings().get_cancel_flag()) {
return lia_move::undef;
}
if (r == lia_move::conflict || r == lia_move::undef) { if (r == lia_move::conflict || r == lia_move::undef) {
break; break;
} }
@ -1913,7 +1915,8 @@ namespace lp {
if (r == lia_move::conflict) { if (r == lia_move::conflict) {
if (m_conflict_index != UINT_MAX) { if (m_conflict_index != UINT_MAX) {
lra.stats().m_dio_rewrite_conflicts++; lra.stats().m_dio_rewrite_conflicts++;
} else { }
else {
lra.stats().m_dio_bound_propagation_conflicts++; lra.stats().m_dio_bound_propagation_conflicts++;
} }
return lia_move::conflict; return lia_move::conflict;