ebmc: test for k-induction with both refuted and proved property

regression/ebmc/k-induction/k-induction5.desc

@@ -0,0 +1,9 @@
+CORE
+k-induction5.v
+--module main --bound 1 --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^\[main.property.property1\] .* SUCCESS$
+^\[main.property.property2\] .* FAILURE$
+--
+^warning: ignoring

regression/ebmc/k-induction/k-induction5.v

@@ -0,0 +1,21 @@
+module main();
+
+  reg [31:0] x, y;
+  wire clk;
+
+  initial x=1;
+  initial y=1;
+
+  always @(posedge clk)
+    if(x<1000) begin
+      x<=x+1;
+      y<=y+1;
+    end
+
+  // true, and 1-inductive
+  always assert property1: x<=1000;
+
+  // false, bound 1 suffices
+  always assert property2: x!=2;
+
+endmodule