mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

updated logging

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-10-06 18:02:20 -07:00
parent 546e152837
commit ae7d76767b
2 changed files with 6 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/fingerprints.cpp
View file

@ -66,18 +66,13 @@ namespace smt {
fingerprint * d = mk_dummy(data, data_hash, num_args, args);
if (m_set.contains(d))
return nullptr;
TRACE("fingerprint_bug", tout << "1) inserting: " << data_hash << " num_args: " << num_args;
for (unsigned i = 0; i < num_args; i++) tout << " " << args[i]->get_owner_id();
tout << "\n";);
for (unsigned i = 0; i < num_args; i++)
d->m_args[i] = d->m_args[i]->get_root();
if (m_set.contains(d)) {
TRACE("fingerprint_bug", tout << "failed: " << data_hash << " num_args: " << num_args;
for (unsigned i = 0; i < num_args; i++) tout << " " << d->m_args[i]->get_owner_id();
tout << "\n";);
TRACE("fingerprint_bug", tout << "failed: " << *d;);
return nullptr;
}
TRACE("fingerprint_bug", tout << "2) inserting: " << *d;);
TRACE("fingerprint_bug", tout << "inserting @" << m_scopes.size() << " " << *d;);
fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, def, num_args, d->m_args);
m_fingerprints.push_back(f);
m_defs.push_back(def);
@ -117,6 +112,7 @@ namespace smt {
m_fingerprints.shrink(old_size);
m_defs.shrink(old_size);
m_scopes.shrink(new_lvl);
TRACE("fingerprint_bug", tout << "pop @" << m_scopes.size() << "\n";);
}
void fingerprint_set::display(std::ostream & out) const {

6
src/smt/smt_quantifier.cpp
View file

@ -313,10 +313,10 @@ namespace smt {
m_num_instances++;
}
CTRACE("quantifier_", f != nullptr,
tout << expr_ref(q, m()) << " ";
CTRACE("bindings", f != nullptr,
tout << expr_ref(q, m()) << "\n";
for (unsigned i = 0; i < num_bindings; ++i) {
tout << expr_ref(bindings[i]->get_owner(), m()) << " ";
tout << expr_ref(bindings[i]->get_owner(), m()) << " [r " << bindings[i]->get_root()->get_owner_id() << "] ";
}
tout << "\n";
);