From 1d5fafd5580956d31b4b7617d38c7b4d564066f9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 10 May 2017 21:18:20 -0700 Subject: [PATCH] disable lev's solver Signed-off-by: Lev Nachmanson --- 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 25b11b7fb..7fe26bd22 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -720,10 +720,10 @@ namespace smt { } void setup::setup_r_arith() { - //m_context.register_plugin(alloc(smt::theory_mi_arith, 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)); + // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } void setup::setup_mi_arith() {