ebmc: Downgrade level of progress output during unwinding

The progress output during unwinding is downgraded from 'status' to the 'progress' verbosity level.
diffblue · Dec 6, 2023 · 54ce2d6 · 54ce2d6
1 parent eac3a72
commit 54ce2d6
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/src/trans-netlist/unwind_netlist.cpp b/src/trans-netlist/unwind_netlist.cpp
@@ -37,17 +37,17 @@ void unwind(
   if(add_initial_state && first)
   {
     // do initial state
-    message.status() << "Initial State" << messaget::eom;
+    message.progress() << "Initial State" << messaget::eom;
 
     for(const auto & n : netlist.initial)
       solver.l_set_to(bmc_map.translate(0, n), true);
   }
 
   // do transitions
   if(last)
-    message.status() << "Transition " << t << messaget::eom;
+    message.progress() << "Transition " << t << messaget::eom;
   else
-    message.status() << "Transition " << t << "->" << t+1 << messaget::eom;
+    message.progress() << "Transition " << t << "->" << t+1 << messaget::eom;
 
   const bmc_mapt::timeframet &timeframe=bmc_map.timeframe_map[t];
 

diff --git a/src/trans-word-level/unwind.cpp b/src/trans-word-level/unwind.cpp
@@ -40,7 +40,7 @@ void unwind(
 
   // in-state constraints
 
-  message.status() << "In-state constraints" << messaget::eom;
+  message.progress() << "In-state constraints" << messaget::eom;
 
   if(!op_invar.is_true())
     for(std::size_t c = 0; c < no_timeframes; c++)
@@ -51,7 +51,7 @@ void unwind(
 
   if(initial_state)
   {
-    message.status() << "Initial state" << messaget::eom;
+    message.progress() << "Initial state" << messaget::eom;
 
     if(!op_init.is_true())
       decision_procedure.set_to_true(
@@ -60,7 +60,7 @@ void unwind(
 
   // transition relation
 
-  message.status() << "Transition relation" << messaget::eom;
+  message.progress() << "Transition relation" << messaget::eom;
 
   if(!op_trans.is_true())
     for(std::size_t t = 0; t < no_timeframes; t++)
@@ -69,9 +69,9 @@ void unwind(
       bool last=(t==no_timeframes-1);
 
       if(last)
-        message.status() << "Transition " << t << messaget::eom;
+        message.progress() << "Transition " << t << messaget::eom;
       else
-        message.status() << "Transition " << t << "->" << t+1 << messaget::eom;
+        message.progress() << "Transition " << t << "->" << t+1 << messaget::eom;
 
       decision_procedure.set_to_true(
         instantiate(op_trans, t, no_timeframes, ns));