diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp
index 78978ce4c..000193563 100644
--- a/src/math/grobner/pdd_solver.cpp
+++ b/src/math/grobner/pdd_solver.cpp
@@ -311,6 +311,7 @@ namespace dd {
             unsigned v = m_level2var[m_levelp1-1];
             equation* eq = nullptr;
             for (equation* curr : m_to_simplify) {
+                SASSERT(curr->idx() != UINT_MAX);
                 pdd const& p = curr->poly();
                 if (curr->state() == to_simplify && p.var() == v) {
                     if (!eq || is_simpler(*curr, *eq))
@@ -389,6 +390,16 @@ namespace dd {
         retire(eq);
     }
 
+    void solver::retire(equation* eq) { 
+#if 0
+        // way to check if retired equations are ever accessed.
+        eq->set_index(UINT_MAX);
+#else
+        dealloc(eq); 
+#endif
+    }
+
+
     void solver::pop_equation(equation& eq) {
         equation_vector& v = get_queue(eq);
         unsigned idx = eq.idx();
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index cceb34b0b..150a70df8 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -181,7 +181,7 @@ private:
     void del_equation(equation& eq) { del_equation(&eq); }    
     void del_equation(equation* eq);    
     equation_vector& get_queue(equation const& eq);
-    void retire(equation* eq) { dealloc(eq); }
+    void retire(equation* eq);
     void pop_equation(equation& eq);
     void pop_equation(equation* eq) { pop_equation(*eq); }
     void push_equation(eq_state st, equation& eq);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 241948c41..00db7bc42 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -892,10 +892,6 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const {
     return true;
 }
 
-void core::negate_var_relation_strictly(new_lemma& lemma, lpvar a, lpvar b) {
-    SASSERT(val(a) != val(b));
-    lemma |= ineq(term(a, -rational(1), b), val(a) < val(b) ? llc::GT : llc::LT, 0);
-}
 
 void core::negate_factor_equality(new_lemma& lemma, const factor& c,
                                   const factor& d) {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 170ef52b9..07cbc7c27 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -426,7 +426,6 @@ public:
     void negate_relation(new_lemma& lemma, unsigned j, const rational& a);
     void negate_factor_equality(new_lemma& lemma, const factor& c, const factor& d);    
     void negate_factor_relation(new_lemma& lemma, const rational& a_sign, const factor& a, const rational& b_sign, const factor& b);
-    void negate_var_relation_strictly(new_lemma& lemma, lpvar a, lpvar b);
 
     bool  find_bfc_to_refine_on_monic(const monic&, factorization & bf);
     
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 6930bc9c0..5be9a1eea 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -227,25 +227,22 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
     }
 }
 
-bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k) {
+void order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k) {
     const factor c = ac[k];
     TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
     if (c.is_var()) {
         TRACE("nla_solver", tout << "var(c) = " << var(c););
         for (monic const& bc : _().emons().get_use_list(c.var())) {
-            if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) {
-                return true;
-            }
+            if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) 
+                return;
         }
     } 
     else {
         for (monic const& bc : _().emons().get_products_of(c.var())) {
-            if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) {
-                return true;
-            }
+            if (order_lemma_on_ac_and_bc(rm, ac, k, bc)) 
+                return;
         }
     }
-    return false;
 }
 
 void order::generate_ol_eq(const monic& ac,                     
@@ -280,15 +277,19 @@ void order::generate_ol(const monic& ac,
                         const factor& b) {
     
     new_lemma lemma(_(), __FUNCTION__);
-    IF_VERBOSE(100, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac 
+    TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););        
+    IF_VERBOSE(10, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac 
                << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
                << " a " << "*v" << var(a) << " " << val(a) << "\n"
                << " b " << "*v" << var(b) << " " << val(b) << "\n"
                << " c " << "*v" << var(c) << " " << val(c) << "\n");
-    // fix the sign of c
+    // c > 0 and ac >= bc => a >= b
+    // c > 0 and ac <= bc => a <= b
+    // c < 0 and ac >= bc => a <= b
+    // c < 0 and ac <= bc => a >= b
     lemma |= ineq(c.var(), val(c.var()).is_neg() ? llc::GE : llc::LE, 0);
-    _().negate_var_relation_strictly(lemma, ac.var(), bc.var());
-    _().negate_var_relation_strictly(lemma, a.var(),  b.var());
+    lemma |= ineq(term(ac.var(), -rational(1), bc.var()), val(ac.var()) < val(bc.var()) ? llc::GT : llc::LT, 0);
+    lemma |= ineq(term(a.var(),  -rational(1), b.var()),  val(a.var())  < val(b.var())  ? llc::GE : llc::LE, 0);
 
     lemma &= ac;
     lemma &= a;
@@ -298,8 +299,9 @@ void order::generate_ol(const monic& ac,
 }
 
 // We have ac = a*c and bc = b*c.
-// Suppose ac >= bc, then ac/|c| >= bc/|b|
-// Notice that ac/|c| = a*rat_sign(val(c)|, and similar fo bc/|c|.// 
+// Suppose ac >= bc, then ac/|c| >= bc/|c|
+// Notice that ac/|c| = a*rat_sign(val(c)|, and similar fo bc/|c|.
+// 
 bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
                                                  const factor& a,
                                                  const factor& c,
@@ -309,16 +311,14 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
     rational c_sign = rational(nla::rat_sign(val(c)));
     auto av_c_s = val(a) * c_sign;
     auto bv_c_s = val(b) * c_sign;        
-    if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s)
-        ||
+    if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s) ||
         (var_val(ac) < var_val(bc) && av_c_s > bv_c_s)) {
-        TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););        
         generate_ol(ac, a, c, bc, b);
         return true;
-    } else {
-        if ((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) {
-            generate_ol_eq(ac, a, c, bc, b);
-        }
+    } 
+    else if ((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) {
+        generate_ol_eq(ac, a, c, bc, b);
+        return true;
     }
     return false;
 }
diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h
index 272a070dc..c6961bc52 100644
--- a/src/math/lp/nla_order_lemmas.h
+++ b/src/math/lp/nla_order_lemmas.h
@@ -34,7 +34,7 @@ private:
                                   bool k,
                                   const monic& rm_bd);
     
-    bool order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k);
+    void order_lemma_on_ac_explore(const monic& rm, const factorization& ac, bool k);
 
     void order_lemma_on_factorization(const monic& rm, const factorization& ab);