mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

Output both Nielsen graph size and conflict size

Browse source
This commit is contained in:
CEisenhofer 2026-04-01 10:23:55 +02:00
parent 5d95f44a03
commit 60913f0068
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_nseq.cpp
View file

@ -718,6 +718,11 @@ namespace smt {
}
std::cout << std::endl;
#endif
#endif
#ifdef Z3DEBUG
std::cout << "Conflict with " << lits.size() << " literals and " << eqs.size() << " equalities" << std::endl;
std::cout << "The root node contained " << m_nielsen.root()->str_mems().size() << " memberships and " << m_nielsen.root()->str_eqs().size() << " equalities" << std::endl;
#endif
}