From 67eaff44900137c070c4aba3167df40aa38347d9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 10 Jun 2020 16:15:04 -0700 Subject: [PATCH] testing cheap equalities Signed-off-by: Lev Nachmanson --- src/math/lp/lp_bound_propagator.h | 2 +- src/smt/smt_setup.cpp | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 96b4446c4..a51b0fe41 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -216,7 +216,7 @@ public: else return false; } - if (x_index == UINT_MAX && y_index == UINT_MAX) + if (x_index == UINT_MAX || y_index == UINT_MAX) return false; if (lp().column_is_int(row[x_index].var()) != lp().column_is_int(row[y_index].var())) return false; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 8330ca98d..96e46dbbf 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -755,10 +755,10 @@ namespace smt { } void setup::setup_lra_arith() { - // if (m_params.m_arith_mode == AS_OLD_ARITH) - // m_context.register_plugin(alloc(smt::theory_mi_arith, m_context)); - // else - m_context.register_plugin(alloc(smt::theory_lra, m_context)); + if (m_params.m_arith_mode == AS_OLD_ARITH) + m_context.register_plugin(alloc(smt::theory_mi_arith, m_context)); + else + m_context.register_plugin(alloc(smt::theory_lra, m_context)); } void setup::setup_mi_arith() {