mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #5382

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-05 19:30:03 +02:00
parent 7255a2afd1
commit e5aa02b8f5
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/normal_forms/pull_quant.cpp
View file

@ -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) {