mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 04:48:45 +00:00
fix #6081
This commit is contained in:
parent
cc045debac
commit
fe08c9976e
|
@ -2412,7 +2412,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
|
|||
|
||||
static void trace_quant(std::ostream& strm, quantifier* q) {
|
||||
strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
|
||||
<< " #" << q->get_id() << " " << q->get_qid() << " " << q->get_num_decls();
|
||||
<< " #" << q->get_id() << " " << ensure_quote(q->get_qid()) << " " << q->get_num_decls();
|
||||
for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
|
||||
strm << " #" << q->get_pattern(i)->get_id();
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue