@@ -109,7 +109,7 @@ void report_results(
109109
110110 switch (property.status )
111111 {
112- // clang-format off
112+ // clang-format off
113113 case statust::ASSUMED: message.result () << messaget::blue; break ;
114114 case statust::PROVED: message.result () << messaget::green; break ;
115115 case statust::PROVED_WITH_BOUND: message.result () << messaget::green; break ;
@@ -139,9 +139,8 @@ void report_results(
139139
140140 if (property.has_witness_trace ())
141141 {
142- auto term = [&property]() {
143- return property.is_exists_path () ? " Trace" : " Counterexample" ;
144- };
142+ auto term = [&property]()
143+ { return property.is_exists_path () ? " Trace" : " Counterexample" ; };
145144
146145 if (cmdline.isset (" trace" ))
147146 {
@@ -176,19 +175,32 @@ void report_results(
176175
177176 if (cmdline.isset (" vcd" ))
178177 {
178+ const auto outfile_prefix = [&cmdline]() -> std::optional<std::string> {
179+ if (cmdline.isset (" vcd" ))
180+ return cmdline.get_value (" vcd" ) + " ." ;
181+ else
182+ return {};
183+ }();
184+
179185 for (const auto &property : result.properties )
180186 {
181187 if (property.has_witness_trace ())
182188 {
183- std::stringstream vcdfile;
184-
185- vcdfile << property.name << " _witness.vcd" ;
186- auto outfile = output_filet{vcdfile.str ()};
187- std::cout << " Writing witness trace VCD file to " << vcdfile.str () << " \n " ;
189+ std::stringstream vcdfile;
190+ vcdfile << property.name << " _witness.vcd" ;
191+ std::string filename;
192+ if (outfile_prefix.has_value ()) {
193+ filename = outfile_prefix.value () + vcdfile.str ();
194+ } else {
195+ filename = vcdfile.str ();
196+ }
197+
198+ auto outfile = output_filet{filename};
199+ std::cout << " Writing witness trace VCD file to " << filename
200+ << " \n " ;
188201 messaget message (message_handler);
189202 show_trans_trace_vcd (
190203 property.witness_trace .value (), message, ns, outfile.stream ());
191-
192204 }
193205 }
194206 }
0 commit comments