diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 8c29e499d..56d07a5c2 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -251,7 +251,6 @@ struct propagate_ineqs_tactic::imp {
         a_var x = mk_linear_pol(lhs);
         mpq c_prime;
         nm.set(c_prime, c.to_mpq());
-        verbose_stream() << mk_ismt2_pp(t, m) << " bound " << c << "\n";
         if (k == EQ) {
             SASSERT(!strict);
             bp.assert_lower(x, c_prime, false);