diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index 2bf6850d56..a8ad720b07 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -540,7 +540,7 @@ bool pattern_inference_cfg::is_forbidden(app * n) const {
     // Remark: skolem constants should not be used in patterns, since they do not
     // occur outside of the quantifier. That is, Z3 will never match this kind of
     // pattern.
-    if (false && m_params.m_pi_avoid_skolems && decl->is_skolem()) {
+    if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
         CTRACE(pattern_inference_skolem, decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
         return true;
     }