diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b0ba51129..9c6d3f89a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1461,7 +1461,7 @@ public: return atom; } - bool all_variables_have_bounds() { + bool make_sure_all_vars_have_bounds() { if (!m_has_int) { return true; } @@ -1595,10 +1595,6 @@ public: TRACE("arith", tout << "canceled\n";); return l_undef; } - if (!all_variables_have_bounds()) { - TRACE("arith", tout << "not all variables have bounds\n";); - return l_false; - } if (!check_idiv_bounds()) { TRACE("arith", tout << "idiv bounds check\n";); return l_false;