diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index 1604db161..30b4dbfc6 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -26,10 +26,6 @@ Author:
 namespace opt {
 
     bool is_maxlex(weights_t & _ws) {
-        // disable for now
-#if true
-        return false;
-#else
         vector<rational> ws(_ws);
         std::sort(ws.begin(), ws.end());
         ws.reverse();
@@ -42,7 +38,6 @@ namespace opt {
             sum -= w;
         }
         return true;
-#endif
     }
 
     class maxlex : public maxsmt_solver_base {
@@ -141,7 +136,7 @@ namespace opt {
                 if (soft.value == l_true) {
                     continue;
                 }
-                SASSERT(soft.value() == l_undef);
+                SASSERT(soft.value == l_undef);
                 expr* a = soft.s;                
                 lbool is_sat = s().check_sat(1, &a);
                 switch (is_sat) {
@@ -169,7 +164,7 @@ namespace opt {
                 if (soft.value != l_undef) {
                     continue;
                 }
-                SASSERT(soft.value() == l_undef);
+                SASSERT(soft.value == l_undef);
                 if (i + 1 == sz) {
                     expr* a = soft.s;                
                     lbool is_sat = s().check_sat(1, &a);
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 329e7979c..5441c4def 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -232,10 +232,11 @@ namespace opt {
     lbool maxsmt::operator()() {
         lbool is_sat = l_undef;
         m_msolver = nullptr;
+        opt_params optp(m_params);
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
         TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
-        if (is_maxlex(m_weights)) {
+        if (optp.maxlex_enable() && is_maxlex(m_weights)) {
             m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
         }
         else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 623eefea3..4235deb3d 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -14,6 +14,7 @@ def_module_params('opt',
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
                           ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
+                          ('maxlex.enable', BOOL, False, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
                           ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
                           ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
                           ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),