mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity

remove debug instruction

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-04 11:39:29 -10:00
parent 83de6d7e6b
commit 860ccfbac0
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_solver.cpp
View file

@ -1174,10 +1174,10 @@ namespace nlsat {
used_vars[v] = true; used_vars[v] = true;
} }
display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n"; display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
if (m_lemma_count == 60) { /* if (m_lemma_count == 60) {
enable_trace("lws"); enable_trace("lws");
enable_trace("nlsat_explain"); enable_trace("nlsat_explain");
} }*/
if (m_log_lemma_smtrat) if (m_log_lemma_smtrat)
out << "(set-logic NRA)\n"; out << "(set-logic NRA)\n";
else else
@ -1191,10 +1191,10 @@ namespace nlsat {
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
display_smt2(out << "(assert ", ~cls[i]) << ")\n"; display_smt2(out << "(assert ", ~cls[i]) << ")\n";
out << "(check-sat)\n(reset)\n"; out << "(check-sat)\n(reset)\n";
if (m_lemma_count == 62) { /* if (m_lemma_count == 62) {
std::cout << "early exit\n"; std::cout << "early exit\n";
exit(1); exit(1);
} } */
} }
clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {