diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 16d4e3768..59dc1948f 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -145,7 +145,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
                     break;
                 }
                 SASSERT(it_a == a_end && it_b == b_end);
-                ret = a->coeff() < b->coeff();
+                ret = a->coeff() > b->coeff();
                 break;
             }
             if (it_b == b_end) { // it_a is not at the end
@@ -155,7 +155,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
             // no iterator reached the end
             continue;
         }            
-        if (a_pow < b_pow) {
+        if (a_pow > b_pow) {
             it_a++;
             if (it_a == a_end) {
                 ret = true;
@@ -165,7 +165,7 @@ bool nex_creator::less_than_on_mul_mul_same_degree_iterate(const nex_mul* a, con
             inside_b_p = true;
             b_pow -= a_pow;
         } else {
-            SASSERT(a_pow > b_pow);
+            SASSERT(a_pow < b_pow);
             a_pow -= b_pow;
             it_b++;
             if (it_b == b_end) {
@@ -194,9 +194,9 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
     unsigned b_deg = b->get_degree();
     bool ret;
     if (a_deg > b_deg) {
-        ret = false;
-    } else if (a_deg < b_deg) {
         ret = true;
+    } else if (a_deg < b_deg) {
+        ret = false;
     } else {
         ret = less_than_on_mul_mul_same_degree(a, b);
     }
@@ -207,13 +207,13 @@ bool nex_creator::less_than_on_mul_mul(const nex_mul* a, const nex_mul* b) const
 
 bool nex_creator::less_than_on_var_nex(const nex_var* a, const nex* b) const {
     switch(b->type()) {
-    case expr_type::SCALAR: return false;
+    case expr_type::SCALAR: return true;
     case expr_type::VAR:            
         return less_than(a->var() , to_var(b)->var());
     case expr_type::MUL:
         {
             if (b->get_degree() > 1)
-                return true;
+                return false;
             auto it = to_mul(b)->begin();
             const nex_pow & c  = *it;
             const nex * f = c.e();
@@ -236,10 +236,12 @@ bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
     case expr_type::VAR:            
         {
             if (a->get_degree() > 1)
-                return false;
+                return true;
             auto it = a->begin();
             const nex_pow & c  = *it;
+            SASSERT(c.pow() == 1);
             const nex * f = c.e();
+            SASSERT(!f->is_scalar());
             return lt(f, b);
         }
     case expr_type::MUL:
@@ -260,7 +262,7 @@ bool nex_creator::less_than_on_sum_sum(const nex_sum* a, const nex_sum* b) const
         if (lt((*b)[j], (*a)[j]))
             return false;
     }
-    return size < b->size();
+    return size > b->size();
             
 }
 
@@ -275,9 +277,9 @@ bool nex_creator::lt(const nex* a, const nex* b) const {
         break;
     case expr_type::SCALAR: {
         if (b->is_scalar())
-            ret = to_scalar(a)->value() < to_scalar(b)->value();
+            ret = to_scalar(a)->value() > to_scalar(b)->value();
         else
-            ret = true; // the scalars are the smallest
+            ret = false; // the scalars are the largest
         break;
     }        
     case expr_type::MUL: {
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index dbf47c0d4..6e7235fb3 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -86,11 +86,11 @@ public:
     bool less_than(lpvar j, lpvar k) const{
         unsigned wj = (unsigned)m_active_vars_weights[j];
         unsigned wk = (unsigned)m_active_vars_weights[k];
-        return wj != wk ? wj < wk : j < k;
+        return wj != wk ? wj > wk : j > k;
     }
 
     bool less_than_on_nex_pow(const nex_pow & a, const nex_pow& b) const {
-        return (a.pow() < b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e()));
+        return (a.pow() > b.pow()) || (a.pow() == b.pow() && lt(a.e(), b.e()));
     }
     
     void simplify_children_of_mul(vector<nex_pow> & children, rational&);
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index eecfe172a..3f5c2e106 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -82,11 +82,16 @@ void test_nex_order() {
     nex_creator r;
     r.set_number_of_vars(3);
     for (unsigned j = 0; j < r.get_number_of_vars(); j++)
-        r.set_var_weight(j, j);
+        r.set_var_weight(j, 10 - j);
     nex_var* a = r.mk_var(0);
     nex_var* b = r.mk_var(1);
     nex_var* c = r.mk_var(2);
     SASSERT(r.lt(a, b));
+    SASSERT(r.lt(b, c));
+    SASSERT(r.lt(a, c));
+    
+
+    
     nex* ab = r.mk_mul(a, b);
     nex* ba = r.mk_mul(b, a);
     nex* ac = r.mk_mul(a, c);
@@ -96,14 +101,18 @@ void test_nex_order() {
     nex* _2ab = r.mk_mul(rational(2), a, b);
     SASSERT(r.lt(ab, _3ac));
     SASSERT(!r.lt(_3ac, ab));
-    SASSERT(r.lt(a, ab));
-    SASSERT(!r.lt(ab, a));
+    SASSERT(!r.lt(a, ab));
+    SASSERT(r.lt(ab, a));
     SASSERT(r.lt(_2ab, _3ac));
     SASSERT(!r.lt(_3ac, _2ab));
     nex* _2a = r.mk_mul(rational(2), a);
-    SASSERT(r.lt(_2a, _2ab));
-    SASSERT(!r.lt(_2ab, _2a));
+    SASSERT(!r.lt(_2a, _2ab));
+    SASSERT(r.lt(_2ab, _2a));
     SASSERT(nex_creator::equal(ab, ba));
+    nex_sum * five_a_pl_one = r.mk_sum(r.mk_mul(rational(5), a), r.mk_scalar(rational(1)));
+    nex_mul * poly = r.mk_mul(five_a_pl_one, b);
+    nex * p = r.simplify(poly);
+    std::cout << "poly = " << *poly << " , p = " << *p << "\n";
 }
 
 void test_simplify() {