diff --git a/regression/ebmc/k-induction/k-induction5.desc b/regression/ebmc/k-induction/k-induction5.desc
new file mode 100644
index 000000000..b63d64e23
--- /dev/null
+++ b/regression/ebmc/k-induction/k-induction5.desc
@@ -0,0 +1,9 @@
+CORE
+k-induction5.v
+--module main --bound 1 --k-induction
+^EXIT=0$
+^SIGNAL=0$
+^\[main.property.property1\] .* SUCCESS$
+^\[main.property.property2\] .* FAILURE$
+--
+^warning: ignoring
diff --git a/regression/ebmc/k-induction/k-induction5.v b/regression/ebmc/k-induction/k-induction5.v
new file mode 100644
index 000000000..8eb68bbbd
--- /dev/null
+++ b/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