diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 09f020ca6..bfe39e3ae 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -54,7 +54,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         }
         func_decl_info info(m_family_id, k, 1, parameters);
         return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
-    }
+    }      
     case OP_PB_GE:
     case OP_PB_LE: 
     case OP_PB_EQ: {
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 3413d5e6a..e3ca12b73 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -26,4 +26,5 @@ def_module_params('sat',
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
                           ('drat.check', BOOL, False, 'build up internal proof and check'),
+                          ('cardinality.solver', BOOL, True, 'use cardinality solver'),
                        ))
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 02abebbb5..d2ae541a8 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -82,9 +82,7 @@ public:
         m_num_scopes(0),
         m_dep_core(m),
         m_unknown("no reason given") {
-        m_params.set_bool("elim_vars", false);
-        sat_params p1(m_params);
-        m_solver.updt_params(m_params);
+        updt_params(p);
         init_preprocess();
     }
 
@@ -218,8 +216,10 @@ public:
         m_params.append(p);
         sat_params p1(p);
         m_params.set_bool("elim_vars", false);
+        m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
         m_solver.updt_params(m_params);
         m_optimize_model = m_params.get_bool("optimize_model", false);
+
     }
     virtual void collect_statistics(statistics & st) const {
         if (m_preprocess) m_preprocess->collect_statistics(st);