diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index a8b3abc8a..fec10fe0e 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -184,7 +184,6 @@ struct solver::imp { lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; try { - //verbose_stream() << m_limit. r = m_nlsat->check(); } catch (z3_exception&) { diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 56d8524d4..a73d3e5fb 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -3094,9 +3094,6 @@ namespace upolynomial { A.swap(D); // D is of the form P_{j+1} * P_{j+2} * ... * P_k j++; - if (j > 10000) { - display(verbose_stream(), A) << "\n"; - } } TRACE(factor_bug, tout << "A: "; display(tout, A); tout << "\n";); SASSERT(A.size() == 1 && m().is_one(A[0]));