From b3c6b00da7ca8307d265f02ebb5df12950821267 Mon Sep 17 00:00:00 2001 From: Shashank V M Date: Fri, 3 Oct 2025 20:50:51 +0530 Subject: [PATCH 1/4] Create trace for each cover property --- src/ebmc/report_results.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 8c1fd92b4..8520548b0 100644 --- a/src/ebmc/report_results.cpp +++ b/src/ebmc/report_results.cpp @@ -180,14 +180,15 @@ void report_results( { if(property.has_witness_trace()) { - std::string vcdfile = cmdline.get_value("vcd"); - auto outfile = output_filet{vcdfile}; + std::stringstream vcdfile; + vcdfile << property.name << "_witness.vcd"; + auto outfile = output_filet{vcdfile.str()}; + std::cout << "Writing witness trace VCD file to " << vcdfile.str() << "\n"; messaget message(message_handler); show_trans_trace_vcd( property.witness_trace.value(), message, ns, outfile.stream()); - break; } } } From 47d163dce96161ca709bbd3048699d5400213cd3 Mon Sep 17 00:00:00 2001 From: Shashank V M Date: Sun, 19 Oct 2025 15:31:36 +0530 Subject: [PATCH 2/4] Add prefix of filename argument in VCD trace filename --- src/ebmc/report_results.cpp | 32 ++++++++++++++++++++++---------- 1 file changed, 22 insertions(+), 10 deletions(-) diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 8520548b0..6db1ba1a7 100644 --- a/src/ebmc/report_results.cpp +++ b/src/ebmc/report_results.cpp @@ -109,7 +109,7 @@ void report_results( switch(property.status) { - // clang-format off + // clang-format off case statust::ASSUMED: message.result() << messaget::blue; break; case statust::PROVED: message.result() << messaget::green; break; case statust::PROVED_WITH_BOUND: message.result() << messaget::green; break; @@ -139,9 +139,8 @@ void report_results( if(property.has_witness_trace()) { - auto term = [&property]() { - return property.is_exists_path() ? "Trace" : "Counterexample"; - }; + auto term = [&property]() + { return property.is_exists_path() ? "Trace" : "Counterexample"; }; if(cmdline.isset("trace")) { @@ -176,19 +175,32 @@ void report_results( if(cmdline.isset("vcd")) { + const auto outfile_prefix = [&cmdline]() -> std::optional { + if(cmdline.isset("vcd")) + return cmdline.get_value("vcd") + "."; + else + return {}; + }(); + for(const auto &property : result.properties) { if(property.has_witness_trace()) { - std::stringstream vcdfile; - - vcdfile << property.name << "_witness.vcd"; - auto outfile = output_filet{vcdfile.str()}; - std::cout << "Writing witness trace VCD file to " << vcdfile.str() << "\n"; + std::stringstream vcdfile; + vcdfile << property.name << "_witness.vcd"; + std::string filename; + if (outfile_prefix.has_value()) { + filename = outfile_prefix.value() + vcdfile.str(); + } else { + filename = vcdfile.str(); + } + + auto outfile = output_filet{filename}; + std::cout << "Writing witness trace VCD file to " << filename + << "\n"; messaget message(message_handler); show_trans_trace_vcd( property.witness_trace.value(), message, ns, outfile.stream()); - } } } From 726faf306708240c54fd2550798a7800f7130fe4 Mon Sep 17 00:00:00 2001 From: Shashank V M Date: Tue, 21 Oct 2025 12:15:57 +0530 Subject: [PATCH 3/4] fix: whitespace issue --- src/ebmc/report_results.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 6db1ba1a7..9d3452e6c 100644 --- a/src/ebmc/report_results.cpp +++ b/src/ebmc/report_results.cpp @@ -109,7 +109,7 @@ void report_results( switch(property.status) { - // clang-format off + // clang-format off case statust::ASSUMED: message.result() << messaget::blue; break; case statust::PROVED: message.result() << messaget::green; break; case statust::PROVED_WITH_BOUND: message.result() << messaget::green; break; @@ -140,7 +140,8 @@ void report_results( if(property.has_witness_trace()) { auto term = [&property]() - { return property.is_exists_path() ? "Trace" : "Counterexample"; }; + { return property.is_exists_path() ? "Trace" : "Counterexample"; + }; if(cmdline.isset("trace")) { From 143f3874ce18a47b504a03c49fb33d4cf20576ea Mon Sep 17 00:00:00 2001 From: Shashank V M Date: Tue, 21 Oct 2025 12:19:21 +0530 Subject: [PATCH 4/4] fix: revert accidental code changes --- src/ebmc/report_results.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp index 9d3452e6c..bc62677f0 100644 --- a/src/ebmc/report_results.cpp +++ b/src/ebmc/report_results.cpp @@ -139,8 +139,8 @@ void report_results( if(property.has_witness_trace()) { - auto term = [&property]() - { return property.is_exists_path() ? "Trace" : "Counterexample"; + auto term = [&property]() { + return property.is_exists_path() ? "Trace" : "Counterexample"; }; if(cmdline.isset("trace"))