Searched refs:arith_k_sum_is_small (Results 1 – 4 of 4) sorted by relevance
320 if (!st.m_has_rational && !m_params.m_model && st.arith_k_sum_is_small()) in setup_QF_RDL()379 if (st.arith_k_sum_is_small()) in setup_QF_IDL()429 else if (st.arith_k_sum_is_small()) in setup_QF_UFIDL()786 bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; in setup_arith()
319 if (!st.m_has_rational && !m_params.m_model && st.arith_k_sum_is_small()) in setup_QF_RDL()378 if (st.arith_k_sum_is_small()) in setup_QF_IDL()428 else if (st.arith_k_sum_is_small()) in setup_QF_UFIDL()779 bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; in setup_arith()
154 bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); } in arith_k_sum_is_small() function