mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
199daead50
commit
0bc8518cb5
|
@ -163,12 +163,13 @@ namespace q {
|
|||
|
||||
m_stats.m_num_instances++;
|
||||
|
||||
#if 0
|
||||
std::cout << "instantiate\n";
|
||||
for (unsigned i = 0; i < num_bindings; ++i)
|
||||
std::cout << ctx.bpp(f[i]) << " ";
|
||||
std::cout << "\n";
|
||||
std::cout << mk_pp(q, m) << "\n";
|
||||
|
||||
#endif
|
||||
|
||||
// f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") << "\n";
|
||||
|
||||
|
|
|
@ -245,13 +245,15 @@ namespace smt {
|
|||
|
||||
return;
|
||||
}
|
||||
#if 0
|
||||
std::cout << "instantiate\n";
|
||||
enode_vector _bindings(num_bindings, bindings);
|
||||
for (auto * b : _bindings)
|
||||
std::cout << enode_pp(b, m_context) << " ";
|
||||
std::cout << "\n";
|
||||
std::cout << mk_pp(q, m) << "\n";
|
||||
|
||||
#endif
|
||||
|
||||
TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
|
||||
stat->inc_num_instances();
|
||||
if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {
|
||||
|
|
Loading…
Reference in a new issue