diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index cafc5e3bb..fe4691660 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -19,6 +19,7 @@ Revision History:
 --*/
 #include "sat/sat_probing.h"
 #include "sat/sat_solver.h"
+#include "sat/sat_simplifier_params.hpp"
 
 namespace sat {
     probing::probing(solver & _s, params_ref const & p):
@@ -238,12 +239,13 @@ namespace sat {
         return r;
     }
 
-    void probing::updt_params(params_ref const & p) {
-        m_probing             = p.get_bool("probing", true);
-        m_probing_limit       = p.get_uint("probing_limit", 5000000);
-        m_probing_cache       = p.get_bool("probing_cache", true);
-        m_probing_binary      = p.get_bool("probing_binary", true);
-        m_probing_cache_limit = megabytes_to_bytes(p.get_uint("probing_chache_limit", 1024));
+    void probing::updt_params(params_ref const & _p) {
+        sat_simplifier_params p(_p);
+        m_probing             = p.probing();
+        m_probing_limit       = p.probing_limit();
+        m_probing_cache       = p.probing_cache();
+        m_probing_binary      = p.probing_binary();
+        m_probing_cache_limit = p.probing_cache_limit();
     }
 
     void probing::collect_param_descrs(param_descrs & d) {
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index a8f0db724..b78980774 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/src/sat/sat_simplifier_params.pyg
@@ -23,6 +23,11 @@ def_module_params(module_name='sat',
                           ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
                           ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
-                          ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
+                          ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),                 
+                          ('probing', BOOL, True, 'apply failed literal detection during simplification'),
+                          ('probing_limit', UINT, 5000000, 'limit to the number of probe calls'),
+                          ('probing_cache', BOOL, True, 'add binary literals as lemmas'),
+                          ('probing_cache_limit', UINT, 1024, 'cache binaries unless overall memory usage exceeds cache limit'),
+                          ('probing_binary', BOOL, True, 'probe binary clauses'),
                           ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
                           ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))