Merge pull request #266 from diffblue/k-induction5

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

Author: kroening

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

@@ -0,0 +1,11 @@
+KNOWNBUG
+k-induction5.v
+--module main --bound 1 --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^\[main.property.property1\] .* PROVED$
+^\[main.property.property2\] .* INCONCLUSIVE$
+--
+^warning: ignoring
+--
+The result for property2 should be REFUTED.

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

@@ -0,0 +1,11 @@
+KNOWNBUG
+k-induction5.v
+--module main --bound 3 --k-induction
+^EXIT=10$
+^SIGNAL=0$
+^\[main.property.property1\] .* PROVED$
+^\[main.property.property2\] .* PROVED$
+--
+^warning: ignoring
+--
+The result for property2 should be REFUTED.

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