From dca0fb77c2a7d66c31adc7b9ceab2203ca8277af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2015 15:22:32 -0700 Subject: [PATCH] use same defaults as unstable branch for difference logic configuration Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 13259ed0e..800bcaaed 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -362,9 +362,6 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params)); } - else if (!m_params.m_arith_auto_config_simplex && !is_dense(st)) { - m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params)); - } else { // if (st.m_arith_k_sum < rational(INT_MAX / 8)) { // TRACE("setup", tout << "using small integer simplex...\n";); @@ -416,15 +413,6 @@ namespace smt { return; } } -#if 0 - switch (m_params.m_arith_mode) { - case AS_DIFF_LOGIC: - case AS_DENSE_DIFF_LOGIC: - case AS_UTVPI: - setup_arith(); - return; - } -#endif m_params.m_arith_eq_bounds = true; m_params.m_phase_selection = PS_ALWAYS_FALSE; m_params.m_restart_strategy = RS_GEOMETRIC;