From 6637747fd949d4fc110e86514e7fe3f00a5461d4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 1 Mar 2019 18:34:05 -1000 Subject: [PATCH] no special treatment for NE Signed-off-by: Lev Nachmanson --- src/util/lp/nla_solver.cpp | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 839d03d16..f7f77ca7d 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -508,12 +508,7 @@ struct solver::imp { } void mk_ineq(lp::lar_term& t, llc cmp, const rational& rs, lemma& l) { - if (cmp == llc::NE) { - mk_ineq(t, llc::LT, rs, l); - mk_ineq(t, llc::GT, rs, l); - return; - } - TRACE("nla_solver_details", m_lar_solver.print_term(t, tout << "t = ");); + TRACE("nla_solver_details", m_lar_solver.print_term(t, tout << "t = ");); if (explain_ineq(t, cmp, rs)) { return; }