diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index f6579439d..3998e4214 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -129,7 +129,7 @@ public:
 
     bool contains(lpvar j) const { return j == m_j; }
     int get_degree() const { return 1; }
-    bool virtual is_linear() const { return true; }
+    bool is_linear() const override { return true; }
 };
 
 class nex_scalar : public nex {
@@ -195,8 +195,8 @@ class nex_mul : public nex {
     rational        m_coeff;
     vector<nex_pow> m_children;
 public:
-    virtual const nex* get_child_exp(unsigned j) const { return m_children[j].e(); }
-    virtual unsigned get_child_pow(unsigned j) const { return m_children[j].pow(); }
+    const nex* get_child_exp(unsigned j) const override { return m_children[j].e(); }
+    unsigned get_child_pow(unsigned j) const override { return m_children[j].pow(); }
 
     unsigned number_of_child_powers() const { return m_children.size(); }
 
@@ -391,7 +391,7 @@ public:
 
     void add_child(nex* e) { m_children.push_back(e); }
 #ifdef Z3DEBUG
-    virtual void sort() {
+    void sort() override {
         NOT_IMPLEMENTED_YET();
         /*
         for (nex * c : m_children) {
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 73ce7bd84..574e5a34d 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -196,7 +196,8 @@ bool nex_creator::gt_on_var_nex(const nex_var* a, const nex* b) const {
     case expr_type::MUL: 
         return b->get_degree() <= 1 && gt_on_var_nex(a, (*to_mul(b))[0].e());
     case expr_type::SUM:
-        return !gt((*to_sum(b))[0], a);        
+        SASSERT(b->size() > 1);
+        return gt(a, (*to_sum(b))[0]);        
     default:
         UNREACHABLE();
         return false;