mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 13:41:27 +00:00
Code Activity

remove debug out

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-28 14:24:53 -07:00
parent cfb3ece846
commit 9369a14825
3 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_clause_proof.cpp
View file

@ -195,7 +195,6 @@ namespace smt {
if (m_on_clause_eh) {
// Encode status as an integer flag for simplicity.
unsigned st_code = 0;
IF_VERBOSE(0, if (status::assumption != st) verbose_stream() << "status " << st << "\n");
switch (st) {
case status::assumption: st_code = 1; break;
case status::lemma: st_code = 2; break;

2
src/smt/smt_context.cpp
View file

@ -4386,8 +4386,6 @@ namespace smt {
}
}
#endif
IF_VERBOSE(0, verbose_stream() << "(smt.learned-clause"; verbose_stream() << " :size " << num_lits;
verbose_stream() << " :conflicts " << m_num_conflicts << ")\n";);
mk_clause(num_lits, lits, js, CLS_LEARNED);
if (delay_forced_restart) {
SASSERT(num_lits == 1);

1
src/smt/theory_lra.cpp
View file

@ -3469,7 +3469,6 @@ public:
}
void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
IF_VERBOSE(0, verbose_stream() << "set conflict or lemma " << core << "\n");
reset_evidence();
for (literal lit : core) {
m_core.push_back(lit);