diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 9fcce1fce..10ab3c77b 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -774,8 +774,14 @@ public:
         
         for (expr* _ : core)
             partial.push_back(nullptr);
-            
-        for (unsigned i = 0; i + 1 < core.size(); ++i) {
+
+        std::cout << "Core size " << core.size() << "\n";
+
+        if (core.size() > 2)
+            m_unfold_upper += rational(core.size()-2)*weight;
+        
+        expr* w = nullptr;
+        for (unsigned i = 0; i + 1 < core.size(); i += 2) {
             expr* a = core.get(i);
             expr* b = core.get(i + 1);
             expr* u = mk_fresh_bool("u");
diff --git a/src/opt/maxres.h b/src/opt/maxres.h
index 25ef9bf05..947b60492 100644
--- a/src/opt/maxres.h
+++ b/src/opt/maxres.h
@@ -23,6 +23,10 @@ namespace opt {
 
     maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
 
+    maxsmt_solver_base* mk_maxres_binary(maxsat_context& c, unsigned id, vector<soft>& soft);
+
+    maxsmt_solver_base* mk_maxres_binary_delay(maxsat_context& c, unsigned id, vector<soft>& soft);
+
     maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
 
 };
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 5106c5492..cb8f1d129 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -2,7 +2,7 @@ def_module_params('opt',
                   description='optimization parameters',
                   export=True,
                   params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"),
-                          ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
+                          ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'maxres-bin', 'maxres-bin-delay'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('dump_models', BOOL, False, 'display intermediary models to stdout'),