mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
parent
ce1c8ee9e3
commit
cde3eac7be
|
@ -467,7 +467,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
|
|||
See normalize_expr
|
||||
*/
|
||||
void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
|
||||
TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";);
|
||||
TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n" << mk_pp(def, m_manager) << "\n";);
|
||||
SASSERT(is_macro_head(head, head->get_num_args()) ||
|
||||
is_quasi_macro_ok(head, head->get_num_args(), def));
|
||||
SASSERT(!occurs(head->get_decl(), def));
|
||||
|
|
|
@ -198,6 +198,7 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
|
|||
|
||||
bit_vector v_seen;
|
||||
v_seen.resize(q->get_num_decls(), false);
|
||||
unsigned num_seen = 0;
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
expr* arg = a->get_arg(i);
|
||||
if (!is_var(arg) && !is_ground(arg))
|
||||
|
@ -215,8 +216,11 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
|
|||
var * v = to_var(arg);
|
||||
m_new_vars.push_back(v);
|
||||
v_seen.set(v->get_idx(), true);
|
||||
++num_seen;
|
||||
}
|
||||
}
|
||||
if (num_seen < q->get_num_decls())
|
||||
return false;
|
||||
|
||||
// Reverse the new variable names and sorts. [CMW: There is a smarter way to do this.]
|
||||
vector<symbol> new_var_names_rev;
|
||||
|
|
Loading…
Reference in a new issue