Merge pull request #228 from diffblue/random-long-trace1

ebmc: add a test for randomly generating a trace with 1000 steps

Author: tautschnig

regression/ebmc/random-traces/long_trace1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+long_trace1.v
+--random-traces --number-of-traces 1 --trace-steps 1000
+^Transition system state 0$
+^  main\.some_reg = 0 .*$
+^  main\.increment = 0$
+^Transition system state 1000$
+^  main\.some_reg = 'h1F8 .*$
+^  main\.increment = 1$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/random-traces/long_trace1.v

@@ -0,0 +1,10 @@
+module main(input increment);
+
+  wire clk;
+  reg [31:0] some_reg = 0;
+
+  always @(posedge clk)
+    if(increment)
+      some_reg = some_reg + 1;
+
+endmodule