From e0f1e3cc3eb218c62dfa21069887edd662b6bc20 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 24 Jul 2019 07:41:36 -0700
Subject: [PATCH] produce a lemma on a row when there is no cross nested form

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 1683134f4..64c4e67b1 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -30,7 +30,7 @@ public:
 
     void run() {
         vector<nex*> front;
-        explore_expr_on_front_elem(&m_e, front, true); // true for trivial form - no change
+        explore_expr_on_front_elem(&m_e, front); // true for trivial form - no change
     }
 
     static nex* pop_back(vector<nex*>& front) {
@@ -92,7 +92,7 @@ public:
         f.simplify();
         * c = nex::mul(f, *c);
         TRACE("nla_cn", tout << "common factor=" << f << ", c=" << *c << "\n";);
-        explore_expr_on_front_elem(&(c->children()[1]), front, false);
+        explore_expr_on_front_elem(&(c->children()[1]), front);
         return true;
     }
 
@@ -142,21 +142,19 @@ public:
         return out;
     }
 
-    void explore_expr_on_front_elem(nex* c, vector<nex*>& front, bool trivial_form) {
+    void explore_expr_on_front_elem(nex* c, vector<nex*>& front) {
         SASSERT(c->is_sum());
         auto occurences = get_mult_occurences(*c);
         TRACE("nla_cn", tout << "m_e=" << m_e << "\nc=" << *c << ", c occurences=";
-              dump_occurences(tout, occurences) << "; front:"; print_vector_of_ptrs(front, tout) << "\ntrivial_form=" << trivial_form << "\n";);
+              dump_occurences(tout, occurences) << "; front:"; print_vector_of_ptrs(front, tout) << "\n";);
     
         if (occurences.empty()) {
             if(front.empty()) {
-                if (trivial_form)
-                    return;
                 TRACE("nla_cn", tout << "got the cn form: =" << m_e << "\n";);
                 m_call_on_result(m_e);
             } else {
                 nex* c = pop_back(front);
-                explore_expr_on_front_elem(c, front, trivial_form);     
+                explore_expr_on_front_elem(c, front);     
             }
         } else {
             explore_expr_on_front_elem_occs(c, front, occurences);
@@ -173,7 +171,7 @@ public:
         TRACE("nla_cn", tout << "after split c=" << *c << "\nfront="; print_vector_of_ptrs(front, tout) << "\n";);
         SASSERT(front.size());
         nex* n = pop_back(front); TRACE("nla_cn", tout << "n=" << *n <<"\n";);
-        explore_expr_on_front_elem(n, front, false); // we got a non-trivial_form
+        explore_expr_on_front_elem(n, front);
     }
    static void process_var_occurences(lpvar j, std::unordered_map<lpvar, occ>& occurences) {
         auto it = occurences.find(j);