diff --git a/regression/ebmc/random-traces/counter_with_initial_value.desc b/regression/ebmc/random-traces/counter_with_initial_value.desc
new file mode 100644
index 000000000..7f8b1f1fe
--- /dev/null
+++ b/regression/ebmc/random-traces/counter_with_initial_value.desc
@@ -0,0 +1,16 @@
+CORE broken-smt-backend
+counter_with_initial_value.v
+--random-traces --trace-steps 10 --waveform --number-of-traces 2
+^\*\*\* Trace 1$
+^                0   1   2   3   4   5   6   7   8   9  10$
+^     main.clk                                            $
+^  main\.input1 111 228  22 122 182  95  94 154 131  26  95$
+^main\.some_reg 111 110 109 108 107 106 105 104 103 102 101$
+^\*\*\* Trace 2$
+^                0   1   2   3   4   5   6   7   8   9  10$
+^     main\.clk                                            $
+^  main\.input1 178 105  26  10 251 217  12 188  93  44 170$
+^main\.some_reg 178 177 176 175 174 173 172 171 170 169 168$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/random-traces/counter_with_initial_value.v b/regression/ebmc/random-traces/counter_with_initial_value.v
new file mode 100644
index 000000000..51133720f
--- /dev/null
+++ b/regression/ebmc/random-traces/counter_with_initial_value.v
@@ -0,0 +1,11 @@
+module main(input [7:0] input1);
+
+  wire clk;
+  reg [7:0] some_reg;
+  initial some_reg = input1;
+
+  always @(posedge clk)
+    if(some_reg != 0)
+      some_reg = some_reg - 1;
+
+endmodule
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
index 784f1d8d0..52b80670a 100644
--- a/src/ebmc/random_traces.cpp
+++ b/src/ebmc/random_traces.cpp
@@ -159,8 +159,15 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
   transition_systemt transition_system =
     get_transition_system(cmdline, message_handler);
 
+  if(cmdline.isset("waveform") && cmdline.isset("vcd"))
+    throw ebmc_errort() << "cannot do VCD and ASCII waveform simultaneously";
+
+  auto output = cmdline.isset("waveform") ? random_tracest::WAVEFORM
+                : cmdline.isset("vcd")    ? random_tracest::VCD
+                                          : random_tracest::TRACE;
+
   random_tracest(transition_system, message_handler)(
-    outfile_prefix.has_value() ? random_tracest::VCD : random_tracest::TRACE,
+    output,
     outfile_prefix,
     random_seed,
     number_of_traces,