diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 08336b1e4..6b8181886 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -201,8 +201,10 @@ namespace sat {
             m_pb_solver = PB_SOLVER;
         else if (s == symbol("segmented")) 
             m_pb_solver = PB_SEGMENTED;
+        else if (s == symbol("binary_merge"))
+            m_pb_solver == PB_BINARY_MERGE;        
         else 
-            throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented");
+            throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented, binary_merge");
 
         s = p.pb_resolve();
         if (s == "cardinality") 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index b8d0ca0f5..e9895a051 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -57,7 +57,8 @@ namespace sat {
         PB_CIRCUIT,
         PB_SORTING,
         PB_TOTALIZER,
-        PB_SEGMENTED
+        PB_SEGMENTED,
+        PB_BINARY_MERGE
     };
 
     enum pb_resolve {
@@ -162,7 +163,6 @@ namespace sat {
         bool               m_drat_check_unsat;
         bool               m_drat_check_sat;
         
-        pb_solver          m_pb_solver;
         bool               m_card_solver;
         pb_resolve         m_pb_resolve;
         pb_lemma_format    m_pb_lemma_format;
@@ -182,6 +182,10 @@ namespace sat {
         config(params_ref const & p);
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
+
+    private:
+        pb_solver          m_pb_solver;
+
     };
 };
 
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 9ca1150a9..0cc829379 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -300,11 +300,6 @@ public:
         sat_params p1(p);
         m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
         m_params.set_sym("pb.solver", p1.pb_solver());
-
-        m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER);
-        m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING);
-        m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
-
         m_params.set_bool("xor_solver", p1.xor_solver());
         m_solver.updt_params(m_params);
         m_solver.set_incremental(is_incremental() && !override_incremental());