From e5aa02b8f5edb862c7492ac93cee8d21f7f6ee2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Jul 2021 19:30:03 +0200 Subject: [PATCH] fix #5382 Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/pull_quant.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index e0e2de1f7..209772f3b 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -63,7 +63,7 @@ struct pull_quant::imp { for (unsigned i = 0; i < num_children; i++) { expr * child = children[i]; - if (is_quantifier(child)) { + if (is_quantifier(child) && !is_lambda(child)) { if (!found_quantifier && (is_forall(child) || is_exists(child))) { found_quantifier = true; @@ -184,11 +184,11 @@ struct pull_quant::imp { // Remark: patterns are ignored. // See comment in reduce1_app result = m.mk_forall(var_sorts.size(), - var_sorts.data(), - var_names.data(), - nested_q->get_expr(), - std::min(q->get_weight(), nested_q->get_weight()), - q->get_qid()); + var_sorts.data(), + var_names.data(), + nested_q->get_expr(), + std::min(q->get_weight(), nested_q->get_weight()), + m.is_lambda_def(q) ? symbol("pulled-lambda") : q->get_qid()); } void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) {