From e9a085a0e2e5e43d98f9c8cbe006ee085c0f4ba2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 May 2017 08:23:43 -0700 Subject: [PATCH] enable LRA Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) 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() {