From f176e1e5e56045bb376f1f333195fe9595381d97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 May 2017 08:40:20 -0700 Subject: [PATCH] disable LRA until unit tests are fixed Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 9f90c8801..0a13bfe31 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -721,8 +721,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() {