diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index 84d3893eaeb..c2a3721c419 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -218,8 +218,8 @@ propt::resultt pbs_dimacs_cnft::prop_solve()
   pbfile.close();
 
   // We start counting at 1, thus there is one variable fewer.
-  messaget::status() << (no_variables() - 1) << " variables, " << clauses.size()
-                     << " clauses" << eom;
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << clauses.size() << " clauses" << eom;
 
   const bool result = pbs_solve();
 
diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp
index 08a7b9f0a66..42938c3829a 100644
--- a/src/solvers/sat/satcheck_cadical.cpp
+++ b/src/solvers/sat/satcheck_cadical.cpp
@@ -69,8 +69,8 @@ propt::resultt satcheck_cadicalt::prop_solve()
 {
   INVARIANT(status != statust::ERROR, "there cannot be an error");
 
-  messaget::status() << (no_variables() - 1) << " variables, " << clause_counter
-                     << " clauses" << eom;
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << clause_counter << " clauses" << eom;
 
   if(status == statust::UNSAT)
   {
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index 3de729ae0a0..01ea148fb87 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -137,11 +137,8 @@ propt::resultt satcheck_glucose_baset<T>::prop_solve()
   PRECONDITION(status != statust::ERROR);
 
   // We start counting at 1, thus there is one variable fewer.
-  {
-    messaget::status() <<
-      (no_variables()-1) << " variables, " <<
-      solver->nClauses() << " clauses" << eom;
-  }
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << solver->nClauses() << " clauses" << eom;
 
   try
   {
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
index 68a449809b4..a8e1840dff0 100644
--- a/src/solvers/sat/satcheck_ipasir.cpp
+++ b/src/solvers/sat/satcheck_ipasir.cpp
@@ -97,11 +97,8 @@ propt::resultt satcheck_ipasirt::prop_solve()
 {
   INVARIANT(status!=statust::ERROR, "there cannot be an error");
 
-  {
-    messaget::status() <<
-      (no_variables()-1) << " variables, " <<
-      clause_counter << " clauses" << eom;
-  }
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << clause_counter << " clauses" << eom;
 
   // use the internal representation, as ipasir does not support reporting the
   // status
diff --git a/src/solvers/sat/satcheck_lingeling.cpp b/src/solvers/sat/satcheck_lingeling.cpp
index fdafc97250b..2cc79855d6e 100644
--- a/src/solvers/sat/satcheck_lingeling.cpp
+++ b/src/solvers/sat/satcheck_lingeling.cpp
@@ -72,7 +72,7 @@ propt::resultt satcheck_lingelingt::prop_solve()
     std::string msg=
       std::to_string(no_variables()-1)+" variables, "+
       std::to_string(clause_counter)+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   std::string msg;
diff --git a/src/solvers/sat/satcheck_minisat.cpp b/src/solvers/sat/satcheck_minisat.cpp
index 9c96089d55e..ab6114ac2eb 100644
--- a/src/solvers/sat/satcheck_minisat.cpp
+++ b/src/solvers/sat/satcheck_minisat.cpp
@@ -154,11 +154,8 @@ propt::resultt satcheck_minisat1_baset::prop_solve()
 {
   PRECONDITION(status != ERROR);
 
-  {
-    messaget::status() <<
-      (_no_variables-1) << " variables, " <<
-      solver->nClauses() << " clauses" << messaget::eom;
-  }
+  messaget::statistics() << (_no_variables - 1) << " variables, "
+                         << solver->nClauses() << " clauses" << messaget::eom;
 
   add_variables();
 
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index f3b4c892e07..6f8365ded6a 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -167,11 +167,8 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 
-  {
-    messaget::status() <<
-      (no_variables()-1) << " variables, " <<
-      solver->nClauses() << " clauses" << eom;
-  }
+  messaget::statistics() << (no_variables() - 1) << " variables, "
+                         << solver->nClauses() << " clauses" << eom;
 
   try
   {
diff --git a/src/solvers/sat/satcheck_picosat.cpp b/src/solvers/sat/satcheck_picosat.cpp
index 6e945e3a6dc..126e4572510 100644
--- a/src/solvers/sat/satcheck_picosat.cpp
+++ b/src/solvers/sat/satcheck_picosat.cpp
@@ -73,7 +73,7 @@ propt::resultt satcheck_picosatt::prop_solve()
     std::string msg=
       std::to_string(_no_variables-1)+" variables, "+
       std::to_string(picosat_added_original_clauses(picosat))+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   std::string msg;
diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp
index f535f9efa41..ba56a12919a 100644
--- a/src/solvers/sat/satcheck_zchaff.cpp
+++ b/src/solvers/sat/satcheck_zchaff.cpp
@@ -81,7 +81,7 @@ propt::resultt satcheck_zchaff_baset::prop_solve()
     std::string msg=
       std::to_string(solver->num_variables())+" variables, "+
       std::to_string(solver->clauses().size())+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   SAT_StatusT result=(SAT_StatusT)solver->solve();
diff --git a/src/solvers/sat/satcheck_zcore.cpp b/src/solvers/sat/satcheck_zcore.cpp
index 5869bd17960..707af33bcee 100644
--- a/src/solvers/sat/satcheck_zcore.cpp
+++ b/src/solvers/sat/satcheck_zcore.cpp
@@ -41,7 +41,7 @@ propt::resultt satcheck_zcoret::prop_solve()
     std::string msg=
       std::to_string(no_variables()-1)+" variables, "+
       std::to_string(no_clauses())+" clauses";
-    messaget::status() << msg << messaget::eom;
+    messaget::statistics() << msg << messaget::eom;
   }
 
   // get the core