diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp
index 0e548c8961..98943431a6 100644
--- a/src/params/pattern_inference_params.cpp
+++ b/src/params/pattern_inference_params.cpp
@@ -31,6 +31,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) {
     m_pi_non_nested_arith_weight = p.non_nested_arith_weight();
     m_pi_pull_quantifiers        = p.pull_quantifiers();
     m_pi_warnings                = p.warnings();
+    m_pi_avoid_skolems = p.avoid_skolems();
 }
 
 #define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
@@ -48,4 +49,5 @@ void pattern_inference_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_pi_nopat_weight);
     DISPLAY_PARAM(m_pi_avoid_skolems);
     DISPLAY_PARAM(m_pi_warnings);
+    DISPLAY_PARAM(m_pi_avoid_skolems);
 }
diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg
index 80d36e3ec1..81495c8913 100644
--- a/src/params/pattern_inference_params_helper.pyg
+++ b/src/params/pattern_inference_params_helper.pyg
@@ -11,4 +11,5 @@ def_module_params(class_name='pattern_inference_params_helper',
                           ('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'),
+                          ('avoid_skolems', BOOL, True, 'avoid skolem functions when computing patterns'),
                           ('warnings', BOOL, False, 'enable/disable warning messages in the pattern inference module')))