From 2a63c56ae0aa3e68052247d2c934d7c6a9840e5a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 May 2017 14:03:30 -0700 Subject: [PATCH] A faster and more scalable LRA solver by Lev Nachmanson. It is disabled in the initial merge pending a few bug fixes Signed-off-by: Nikolaj Bjorner --- src/smt/smt_setup.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 1abb3d010..ebb1f87fd 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -720,7 +720,10 @@ namespace smt { } void setup::setup_r_arith() { - 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)); + + // Disabled in initial commit of LRA additions + // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } void setup::setup_mi_arith() {