mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
regressions from previous push
This commit is contained in:
parent
2daf569da6
commit
07c26208fa
|
@ -197,6 +197,7 @@ void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, ex
|
|||
VERIFY(m.is_eq(body, lhs, rhs));
|
||||
SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d));
|
||||
SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d));
|
||||
SASSERT(!is_not || m.is_bool(lhs));
|
||||
if (is_app_of(lhs, d)) {
|
||||
revert = false;
|
||||
head = to_app(lhs);
|
||||
|
|
|
@ -185,6 +185,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
|
|||
return true;
|
||||
}
|
||||
if (m_manager.is_not(n, lhs) && m_manager.is_eq(lhs, lhs, rhs) &&
|
||||
m_manager.is_bool(lhs) &&
|
||||
is_macro_head(lhs, num_decls) &&
|
||||
!is_forbidden(to_app(lhs)->get_decl()) &&
|
||||
!occurs(to_app(lhs)->get_decl(), rhs)) {
|
||||
|
@ -224,6 +225,7 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h
|
|||
return true;
|
||||
}
|
||||
if (m_manager.is_not(n, n) && m_manager.is_eq(n, lhs, rhs) &&
|
||||
m_manager.is_bool(lhs) &&
|
||||
is_macro_head(rhs, num_decls) &&
|
||||
!is_forbidden(to_app(rhs)->get_decl()) &&
|
||||
!occurs(to_app(rhs)->get_decl(), lhs)) {
|
||||
|
|
Loading…
Reference in a new issue