From c3170108e62d18c5f276b593bc241dfe4bf996a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Jul 2026 14:25:20 -0700 Subject: [PATCH] remove ad-hoc disabling skolem shadowing in pattern inference Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/pattern_inference.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; }