mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

formatting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-20 17:16:47 -10:00 • committed by Lev Nachmanson
parent f073da9edd
commit c634701b8f
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2131,14 +2131,15 @@ namespace lp {
do {
init(f_vector);
ret = process_f_and_tighten_terms(f_vector);
} while(ret == lia_move::continue_with_check);
if (ret != lia_move::undef) {
return ret;
}
if (lra.stats().m_dio_calls % lra.settings().dio_branching_period() == 0) {
while (ret == lia_move::continue_with_check);
if (ret != lia_move::undef)
return ret;
if (lra.stats().m_dio_calls % lra.settings().dio_branching_period() == 0)
ret = branching_on_undef();
}
m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2;
return ret;
}