numbered trace output now includes number of states

This enables writing tests that check the length of the witness trace.
diffblue · Apr 22, 2024 · f552b6e · f552b6e
1 parent d3071f4
commit f552b6e
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 3 deletions.
diff --git a/regression/ebmc/smv/smv_ltlspec3.desc b/regression/ebmc/smv/smv_ltlspec3.desc
@@ -4,6 +4,7 @@ smv_ltlspec3.smv
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main::spec1\] X X main::var::x = TRUE: REFUTED$
+^Counterexample with 3 states:$
 ^main::var::x@0 = FALSE$
 ^main::var::x@1 = FALSE$
 ^main::var::x@2 = FALSE$

diff --git a/regression/ebmc/traces/numbered1.desc b/regression/ebmc/traces/numbered1.desc
@@ -4,7 +4,7 @@ waveform1.smv
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main::spec1\] .* REFUTED$
-^Counterexample:$
+^Counterexample with 21 states:$
 ^main::var::y@0 = 0$
 ^main::var::y@10 = 100$
 ^main::var::y@20 = 200$

diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc
@@ -2,7 +2,7 @@ CORE
 cover1.sv
 --bound 10 --numbered-trace
 ^\[main\.property\.p0\] cover main\.counter == 1: PROVED$
-^Trace:$
+^Trace with 2 states:$
 ^main\.counter@0 = 0$
 ^main\.counter@1 = 1$
 ^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$

diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
@@ -135,7 +135,17 @@ void report_results(
         }
         else if(cmdline.isset("numbered-trace"))
         {
-          message.status() << term() << ":" << messaget::eom;
+          message.status() << term();
+          auto failing_opt =
+            property.witness_trace->get_min_failing_timeframe();
+          if(failing_opt.has_value())
+          {
+            if(*failing_opt == 0)
+              message.status() << " with 1 state";
+            else
+              message.status() << " with " << *failing_opt + 1 << " states";
+          }
+          message.status() << ':' << messaget::eom;
           show_trans_trace_numbered(
             property.witness_trace.value(), message, ns, std::cout);
         }