Merge pull request #256 from diffblue/k-induction4

ebmc: add a test for 1-induction

Author: tautschnig

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

@@ -0,0 +1,8 @@
+CORE
+k-induction4.sv
+--module main --bound 1 --k-induction
+^EXIT=0$
+^SIGNAL=0$
+^\[main.property.p1] .* UNKNOWN$
+--
+^warning: ignoring

regression/ebmc/k-induction/k-induction4.sv

@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [31:0] x;
+  
+  initial x=0;
+  
+  always @(posedge clk)
+    if(x != 10)
+      x<=x+1;
+
+  // true but not inductive
+  p1: assert property (x[31] == 0);
+
+endmodule