mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

fix #5152

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-06 11:34:06 -07:00
parent 6099b84ff6
commit a832ada3d1
1 changed files with 5 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -46,7 +46,7 @@ struct pull_quant::imp {
if (m.is_not(d)) { if (m.is_not(d)) {
SASSERT(num_children == 1); SASSERT(num_children == 1);
expr * child = children[0]; expr * child = children[0];
if (is_quantifier(child)) { if (is_quantifier(child) && (is_forall(child) || is_exists(child))) {
quantifier * q = to_quantifier(child); quantifier * q = to_quantifier(child);
expr * body = q->get_expr(); expr * body = q->get_expr();
quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k; quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k;
@ -65,14 +65,12 @@ struct pull_quant::imp {
expr * child = children[i]; expr * child = children[i];
if (is_quantifier(child)) { if (is_quantifier(child)) {
if (!found_quantifier) { if (!found_quantifier && (is_forall(child) || is_exists(child))) {
found_quantifier = true; found_quantifier = true;
forall_children = is_forall(child); forall_children = is_forall(child);
}
else {
// Since the initial formula was in SNF, all children must be EXISTS or FORALL.
SASSERT(forall_children == is_forall(child));
} }
else if (forall_children != is_forall(child))
return false;
quantifier * nested_q = to_quantifier(child); quantifier * nested_q = to_quantifier(child);
if (var_sorts.empty()) { if (var_sorts.empty()) {