Generate VCD file for each cover statement

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,18 +175,32 @@ void report_results(
 
   if(cmdline.isset("vcd"))
   {
+    const auto outfile_prefix = [&cmdline]() -> std::optional<std::string> {
+    if(cmdline.isset("vcd"))
+      return cmdline.get_value("vcd") + ".";
+    else
+      return {};
+    }();
+
     for(const auto &property : result.properties)
     {
       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";
+        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());
-
-        break;
       }
     }
   }