mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

log scope level of lemma

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-07-01 14:14:30 -07:00
parent bfed237a6c
commit a28f55a3bc
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -1063,7 +1063,7 @@ lemma_builder::~lemma_builder() {
if (current().is_conflict()) { if (current().is_conflict()) {
c.m_conflicts++; c.m_conflicts++;
} }
IF_VERBOSE(4, verbose_stream() << name << "\n"); IF_VERBOSE(4, verbose_stream() << name << " " << c.lra.get_scope_level() << "\n");
IF_VERBOSE(4, verbose_stream() << *this << "\n"); IF_VERBOSE(4, verbose_stream() << *this << "\n");
TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; ); TRACE(nla_solver, tout << name << " " << (++i) << "\n" << *this; );
} }