From ab1b2ae86d2c8eb9a94e60726d312c0cb8c0876d Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 3 Apr 2019 21:43:46 -0700
Subject: [PATCH] remove dead code and a fix in no_lemmas_hold

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/tactic/smtlogics/qfnia_tactic.cpp |  3 ++-
 src/util/lp/nla_solver.cpp            | 24 ++++--------------------
 2 files changed, 6 insertions(+), 21 deletions(-)

diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 01e418135..93a284946 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -115,14 +115,15 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
 }
 
 tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
-
     return and_then(
         mk_report_verbose_tactic("(qfnia-tactic)", 10),
         mk_qfnia_premable(m, p),
         // or_else(mk_qfnia_sat_solver(m, p),
         //      try_for(mk_qfnia_smt_solver(m, p), 2000),
         //     mk_qfnia_nlsat_solver(m, p),
+        
                 mk_qfnia_smt_solver(m, p))
         //     )
         ;
 }
+
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 5238c7e8a..308693ad9 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -58,22 +58,6 @@ point operator+(const point& a, const point& b) {
 point operator-(const point& a, const point& b) {
     return point(a.x - b.x, a.y - b.y);
 } 
-
-void divide_by_common_factor(unsigned_vector& a, unsigned_vector& b) {
-    SASSERT(lp::is_non_decreasing(a) && lp::is_non_decreasing(b));
-    unsigned i = 0, j = 0;
-    while (i < a.size() && j < b.size()){
-        if (a[i] == b[j]) {
-            a.erase(a.begin() + i);
-            b.erase(b.begin() + j);
-        } else if (a[i] < b[j]) {
-            i++;
-        } else {
-            j++;
-        }
-    }
-}
-
 struct solver::imp {
     struct bfc {
         lpvar m_x, m_y;
@@ -161,10 +145,10 @@ struct solver::imp {
         return compare_holds(value(t), n.cmp(), n.rs());
     }
 
-    bool an_ineq_holds(const lemma& l) const {
+    bool lemma_holds(const lemma& l) const {
         for(const ineq &i : l.ineqs()) {
-            if (!ineq_holds(i))
-                return false;
+            if (ineq_holds(i))
+                return true;
         }
         return false;
     }
@@ -3126,7 +3110,7 @@ struct solver::imp {
 
     bool no_lemmas_hold() const {
         for (auto & l : * m_lemma_vec) {
-            if (an_ineq_holds(l))
+            if (lemma_holds(l))
                 return false;
         }
         return true;