From eb8da3fb9d9121fc53b0dbdc9178d34c7e1546da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 May 2017 09:34:07 -0700 Subject: [PATCH] fixing setup for LRA, re-enable LRA Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index be6ab3064..4dd1e2510 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -725,8 +725,8 @@ namespace smt { void setup::setup_r_arith() { // to disable theory lra - m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); - // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); + // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); + m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } void setup::setup_mi_arith() { @@ -940,7 +940,7 @@ namespace smt { } if (st.num_theories() == 1 && is_arith(st)) { - if (st.m_has_int && st.m_has_real) + if ((st.m_has_int && st.m_has_real) || (st.m_num_non_linear != 0)) setup_QF_LIRA(st); else if (st.m_has_real) setup_QF_LRA(st);