diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0f1cf30d3..8f014134d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2988,11 +2988,11 @@ public:
         else {
             ci = m_solver->add_var_bound(vi, k, b.get_value());
         }
+        TRACE("arith", tout << "v" << b.get_var() << "\n";);
+        add_ineq_constraint(ci, literal(bv, !is_true));
         if (is_infeasible()) {
             return;
         }
-        TRACE("arith", tout << "v" << b.get_var() << "\n";);
-        add_ineq_constraint(ci, literal(bv, !is_true));
         propagate_eqs(vi, ci, k, b);
     }
 
@@ -3289,7 +3289,7 @@ public:
                 c.neg();
                 ctx().mark_as_relevant(c);
             }
-            TRACE("arith", ctx().display_literals_verbose(tout, m_core););
+            TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
             ctx().mk_th_axiom(get_id(), m_core.size(), m_core.c_ptr());
         }
     }
@@ -3760,6 +3760,8 @@ public:
                 break;
             }
             case null_source:                    
+                out << idx << " null";
+                break;
             default:
                 UNREACHABLE();
                 break; 
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 6d298515a..6165f0bfa 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -519,9 +519,9 @@ struct solver::imp {
     }
 
     void trace_print_monomial_and_factorization(unsigned i_mon, const factorization& f, std::ostream& out) const {
-        out << "mon = ";
-        print_monomial(i_mon, out);
-        out << "\nfact = "; print_factorization(f, out);
+        print_monomial(i_mon, out << "mon:  ") << "\n";
+        out << "value: " << vvr(m_monomials[i_mon].var()) << "\n";
+        print_factorization(f, out << "fact: ") << "\n";
     }
     // x = 0 or y = 0 -> xy = 0
     bool basic_lemma_for_mon_zero_from_factors_to_monomial(unsigned i_mon, const factorization& f) {
@@ -840,11 +840,64 @@ struct solver::imp {
         m_lemma->clear();
     }
 
-    bool order_lemma(const unsigned_vector& to_refine) {
+    bool order_lemma_on_factor(const factorization& f, unsigned k, int sign) {
         return false;
     }
 
+    bool order_lemma_on_factorization(unsigned i_mon, const factorization& f) {
+        for (unsigned k = 0; k < f.size(); k++) {
+            const rational & v = vvr(f[k]);
+            if (v.is_zero())
+                continue;
+
+            int sign = ((v.is_pos() && f.sign().is_pos()) || (v.is_neg() && f.sign().is_neg()))? 1 : -1;
+            
+            if (order_lemma_on_factor(f, k, sign)) { 
+                return true;
+            }
+        }
+        return false;
+    }
+    bool order_lemma_on_monomial(unsigned i_mon) {
+        for (auto factorization : factorization_factory_imp(i_mon, *this)) {
+            if (factorization.is_empty())
+                continue;
+            if (order_lemma_on_factorization(i_mon, factorization))
+                return true;
+        }
+        return false;
+    }
+    
+    bool order_lemma(const unsigned_vector& to_refine) {
+        for (unsigned i_mon : to_refine) {
+            if (order_lemma_on_monomial(i_mon)) {
+                return true;
+            } 
+        }
+        return false;
+    }
+
+    bool monotonicity_lemma_on_factorization(unsigned i_mon, const factorization& factorization) {
+        return false;
+    }
+    
+    bool monotonicity_lemma_on_monomial(unsigned i_mon) {
+        for (auto factorization : factorization_factory_imp(i_mon, *this)) {
+            if (factorization.is_empty())
+                continue;
+            if (monotonicity_lemma_on_factorization(i_mon, factorization))
+                return true;
+        }
+        return false;
+    }
+    
     bool monotonicity_lemma(const unsigned_vector& to_refine) {
+        for (unsigned i_mon : to_refine) {
+            if (monotonicity_lemma_on_monomial(i_mon)) {
+                return true;
+            } 
+        }
+        
         return false;
     }
 
@@ -857,16 +910,20 @@ struct solver::imp {
         m_expl =   &exp;
         m_lemma =  &l;
        
-        if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL)
+        if (m_lar_solver.get_status() != lp::lp_status::OPTIMAL) {
+            TRACE("nla_solver", tout << "unknown\n";);
             return l_undef;
+        }
+
         unsigned_vector to_refine;
         for (unsigned i = 0; i < m_monomials.size(); i++) {
             if (!check_monomial(m_monomials[i]))
                 to_refine.push_back(i);
         }
 
-        if (to_refine.empty())
+        if (to_refine.empty()) {
             return l_true;
+        }
 
         TRACE("nla_solver", tout << "to_refine.size() = " << to_refine.size() << std::endl;);