From 60913f0068587e506b12717486c73fbf19819e76 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 1 Apr 2026 10:23:55 +0200 Subject: [PATCH] Output both Nielsen graph size and conflict size --- src/smt/theory_nseq.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 03d0d39e9..bb9a6ceb0 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -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 }