mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Added diagnostic output for pattern inference.
This commit is contained in:
parent
1620796bd1
commit
3487b368d1
|
@ -729,6 +729,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
|
|||
return;
|
||||
}
|
||||
|
||||
IF_IVERBOSE(10,
|
||||
verbose_stream() << "(smt.inferred-patterns :qid " << q->get_qid() << "\n";
|
||||
for (unsigned i = 0; i < new_patterns.size(); i++)
|
||||
verbose_stream() << " " << mk_ismt2_pp(new_patterns[i], m, 2) << "\n";
|
||||
verbose_stream() << ")\n"; );
|
||||
|
||||
cache_result(q, new_q, pr);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue