From f552b6e0bcd9bf15c99c25f5553cadb135b61865 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 21 Apr 2024 18:09:33 -0700
Subject: [PATCH] numbered trace output now includes number of states

This enables writing tests that check the length of the witness trace.
---
 regression/ebmc/smv/smv_ltlspec3.desc |  1 +
 regression/ebmc/traces/numbered1.desc |  2 +-
 regression/verilog/SVA/cover1.desc    |  2 +-
 src/ebmc/report_results.cpp           | 12 +++++++++++-
 4 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/regression/ebmc/smv/smv_ltlspec3.desc b/regression/ebmc/smv/smv_ltlspec3.desc
index deea00709..0b435985f 100644
--- 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
index fdff9ddf2..7945483aa 100644
--- 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
index 5b49c63d3..f980b8f87 100644
--- 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
index b7f75a9fe..967c64338 100644
--- 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);
         }