diff --git a/src/ast/pattern/pattern_inference_params.h b/src/ast/pattern/pattern_inference_params.h
index 7108e5589..59faa150f 100644
--- a/src/ast/pattern/pattern_inference_params.h
+++ b/src/ast/pattern/pattern_inference_params.h
@@ -19,6 +19,8 @@ Revision History:
 #ifndef _PATTERN_INFERENCE_PARAMS_H_
 #define _PATTERN_INFERENCE_PARAMS_H_
 
+#include"pattern_inference_params_helper.hpp"
+
 enum arith_pattern_inference_kind {
     AP_NO,           // do not infer patterns with arithmetic terms
     AP_CONSERVATIVE, // only infer patterns with arithmetic terms if there is no other option
@@ -37,17 +39,22 @@ struct pattern_inference_params {
     bool                          m_pi_avoid_skolems;
     bool                          m_pi_warnings;
     
-    pattern_inference_params():
-        m_pi_max_multi_patterns(0),
-        m_pi_block_loop_patterns(true),
-        m_pi_arith(AP_CONSERVATIVE),
-        m_pi_use_database(false), 
-        m_pi_arith_weight(5),
-        m_pi_non_nested_arith_weight(10),
-        m_pi_pull_quantifiers(true),
+    pattern_inference_params(params_ref const & p = params_ref()):
         m_pi_nopat_weight(-1),
-        m_pi_avoid_skolems(true),
-        m_pi_warnings(false) {
+        m_pi_avoid_skolems(true) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & _p) {
+        pattern_inference_params_helper p(_p);
+        m_pi_max_multi_patterns      = p.max_multi_patterns();
+        m_pi_block_loop_patterns     = p.block_loop_patterns();
+        m_pi_arith                   = static_cast<arith_pattern_inference_kind>(p.arith());
+        m_pi_use_database            = p.use_database();
+        m_pi_arith_weight            = p.arith_weight();
+        m_pi_non_nested_arith_weight = p.non_nested_arith_weight();
+        m_pi_pull_quantifiers        = p.pull_quantifiers();
+        m_pi_warnings                = p.warnings();
     }
 };
 
diff --git a/src/ast/pattern/pattern_inference_params_helper.pyg b/src/ast/pattern/pattern_inference_params_helper.pyg
new file mode 100644
index 000000000..cc9699b01
--- /dev/null
+++ b/src/ast/pattern/pattern_inference_params_helper.pyg
@@ -0,0 +1,11 @@
+def_module_params(class_name='pattern_inference_params_helper',
+                  module_name='pi',
+                  export=True,
+                  params=(('max_multi_patterns', UINT, 0, 'when patterns are not provided, the prover uses a heuristic to infer them, this option sets the threshold on the number of extra multi-patterns that can be created; by default, the prover creates at most one multi-pattern when there is no unary pattern'),
+                          ('block_loop_patterns', BOOL, True, 'block looping patterns during pattern inference'),
+                          ('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
+                          ('use_database', BOOL, True, 'use pattern database'),
+                          ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
+                          ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
+                          ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),
+                          ('warnings', BOOL, False, 'enable/disable warning messages in the pattern inference module')))