From a323eaf1c849e8012ede4185c42ca1e43b317e17 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sun, 7 Apr 2019 15:35:04 -0700
Subject: [PATCH] add some nla statistics  generate not more than one pl lemma
 an a rm monomial

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp     | 9 +++++++--
 src/util/lp/nla_solver.cpp | 1 +
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index da1204685..5a59cbf57 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -116,6 +116,8 @@ struct stats {
     unsigned m_bound_propagations2;
     unsigned m_assert_diseq;
     unsigned m_gomory_cuts;
+    unsigned m_nla_explanations;
+    unsigned m_nla_lemmas;
     stats() { reset(); }
     void reset() {
         memset(this, 0, sizeof(*this));
@@ -2146,9 +2148,11 @@ public:
     lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& lv) {
         switch (r) {
         case l_false: {
+            m_stats.m_nla_lemmas += lv.size();
             for(const nla::lemma & l : lv) {
-                m_lemma = l; //todo avoit the copy
+                m_lemma = l; //todo avoid the copy
                 m_explanation = l.expl();
+                m_stats.m_nla_explanations += l.expl().size();
                 false_case_of_check_nla();
             }
             break;
@@ -3761,7 +3765,8 @@ public:
         st.update("arith-patches", lp().settings().st().m_patches);
         st.update("arith-patches-success", lp().settings().st().m_patches_success);
         st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls);
-        st.update("arith-hnf-cuts", lp().settings().st().m_hnf_cuts);
+        st.update("nla-explanations", m_stats.m_nla_explanations);
+        st.update("nla-lemmas", m_stats.m_nla_lemmas);
     }        
 };
     
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index dc64e3ab5..736443b06 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -1698,6 +1698,7 @@ struct solver::imp {
         for (factor f : factorization) {
             if (abs(vvr(f)) > rmv) {
                 generate_pl(rm, factorization, factor_index);
+                return;
             }
             factor_index++;
         }