diff --git a/regression/ebmc/k-induction/k-induction4.desc b/regression/ebmc/k-induction/k-induction4.desc
new file mode 100644
index 000000000..a63c8a5a9
--- /dev/null
+++ b/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
diff --git a/regression/ebmc/k-induction/k-induction4.sv b/regression/ebmc/k-induction/k-induction4.sv
new file mode 100644
index 000000000..b4317e94a
--- /dev/null
+++ b/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