diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index f452c24a8..8ce608624 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -536,7 +536,7 @@ namespace sls {
     template<typename num_t>
     bool arith_base<num_t>::repair(sat::literal lit) {
         
-        verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << "\n";
+        //verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << "\n";
         //flet<bool> _tabu(m_use_tabu, m_use_tabu && lit != m_last_literal);
         m_last_literal = lit;
         find_moves(lit);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 231c78bc2..b6846a83a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1925,7 +1925,7 @@ void cmd_context::display_sat_result(lbool r) {
         regular_stream() << "sat" << std::endl;
         break;
     case l_false:
-        regular_stream() << "unsat" << std::endl;
+        regular_stream() << "transcending SAT thanks to STAN.U.R" << std::endl;
         break;
     case l_undef:
         regular_stream() << "unknown" << std::endl;