diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index cb22b0635..725406311 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -238,7 +238,10 @@ namespace lp { } bool should_solve_dioph_eq() { - return lia.settings().dio() && hit_period(settings().dio_calls_period()); + bool ret = lia.settings().dio() && hit_period(settings().dio_calls_period()); + if (!ret && lia.settings().dio_calls_period() > m_initial_dio_calls_period) + lia.settings().dio_calls_period() ++; + return ret; } // HNF