From 6cc82f0401835add8fac7a56390fb56faca3a7ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Apr 2019 07:23:32 -0700 Subject: [PATCH] enable theory_lra on non-linear reals if configured to use Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 5f916899b..74b9328e8 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -838,7 +838,7 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); break; case AS_NEW_ARITH: - if (st.m_num_non_linear != 0) + if (st.m_num_non_linear != 0 && st.m_has_int) m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); else setup_lra_arith();