mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Fix bug reported at http://stackoverflow.com/questions/14307692/unknown-when-using-defs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-13 12:59:39 -08:00
parent 349c21d4de
commit 39d5b850e8
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_setup.cpp
View file

@ -275,7 +275,8 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params));
}
else {
if (m_params.m_arith_auto_config_simplex || st.m_num_uninterpreted_constants > 4 * st.m_num_bool_constants) {
if (m_params.m_arith_auto_config_simplex || st.m_num_uninterpreted_constants > 4 * st.m_num_bool_constants
|| st.m_num_ite_terms > 0 /* theory_rdl and theory_frdl do not support ite-terms */) {
// if (!st.m_has_rational && !m_params.m_model && st.m_arith_k_sum < rational(INT_MAX / 8)) {
// TRACE("rdl_bug", tout << "using theory_smi_arith\n";);
// m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params));