mirror of
https://github.com/Z3Prover/z3
synced 2025-06-05 21:53:23 +00:00
Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable
This commit is contained in:
commit
d3db21ccde
1 changed files with 1 additions and 1 deletions
|
@ -142,7 +142,7 @@ void rule_properties::check_existential_tail() {
|
||||||
todo.push_back(e2);
|
todo.push_back(e2);
|
||||||
}
|
}
|
||||||
else if (is_quantifier(e)) {
|
else if (is_quantifier(e)) {
|
||||||
todo.push_back(to_quantifier(e)->get_expr());
|
tocheck.push_back(to_quantifier(e)->get_expr());
|
||||||
}
|
}
|
||||||
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
|
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
|
||||||
m.is_true(e1)) {
|
m.is_true(e1)) {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue