Merge pull request #286 from diffblue/ic3-unconstrained_initial

ebmc: add a KNOWNBUG test for IC3

Author: tautschnig

regression/ebmc/ic3/unconstrained_initial.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+unconstrained_initial.sv
+--ic3
+^EXIT=1$
+^SIGNAL=0$
+^property FAILED
+^cex verification is ok
+--
+^cex verification failed

regression/ebmc/ic3/unconstrained_initial.sv

@@ -0,0 +1,12 @@
+module main(input clk);
+
+  // no initial state constraint on my_bit
+  reg my_bit;
+
+  always @(posedge clk)
+    my_bit = my_bit;
+
+  // expected to fail
+  p0: assert property (my_bit == 0);
+
+endmodule