diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 5e1fefe8f..688af2d53 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -233,10 +233,7 @@ bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
     case expr_type::MUL:
         return less_than_on_mul(a, to_mul(b));            
     case expr_type::SUM:
-        {
-            const nex* fc = *(to_sum(b)->begin());
-            return lt(a, fc);
-        }
+        return lt(a, (*to_sum(b))[0]);
     default:
         UNREACHABLE();
         return false;
@@ -446,7 +443,7 @@ bool nex_creator::process_mul_in_simplify_sum(nex_mul* em, std::map<nex*, ration
         if (em->size() == 2 && (*em)[1].pow() == 1) {
             found = register_in_join_map(map, (*em)[1].e(), r);
         } else {
-            nex_mul * m = new nex_mul();
+            nex_mul * m = mk_mul();
             for (it++; it != end; it++) {
                 m->add_child_in_power(it->e(), it->pow());
             }
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index 598bf5b26..d09fd2f86 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -96,7 +96,7 @@ public:
     void simplify_children_of_mul(vector<nex_pow> & children);
 
 
-    nex * clone(const nex* a) {
+    nex * clone(const nex* a) {        
         switch (a->type()) {
         case expr_type::VAR: {
             auto v = to_var(a);
@@ -148,7 +148,10 @@ public:
             delete e;
         m_allocated.clear();
     }
-    
+
+    ~nex_creator() {
+        clear();
+    }
     unsigned size() const { return m_allocated.size(); }
     
     nex_sum* mk_sum() {