diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 7fe26bd22..9f90c8801 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -720,10 +720,9 @@ namespace smt { } void setup::setup_r_arith() { - m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); - - // Disabled in initial commit of LRA additions - // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); + // 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)); } void setup::setup_mi_arith() {