diff --git a/regression/ebmc/k-induction/ring_buffer.desc b/regression/ebmc/k-induction/ring_buffer.desc
new file mode 100644
index 000000000..923a9d854
--- /dev/null
+++ b/regression/ebmc/k-induction/ring_buffer.desc
@@ -0,0 +1,10 @@
+CORE
+ring_buffer.sv
+--k-induction
+^\[ring_buffer\.assume\.1\] always \(ring_buffer\.empty \|-> !ring_buffer\.read\): ASSUMED$
+^\[ring_buffer\.assume\.2\] always \(ring_buffer\.full \|-> !ring_buffer\.write\): ASSUMED$
+^\[ring_buffer\.p0\] always \(ring_buffer\.writeptr - ring_buffer\.readptr & 15\) == ring_buffer\.count\[3:0\]: PROVED$
+^\[ring_buffer\.p1\] always ring_buffer\.count <= 16: PROVED$
+^\[ring_buffer\.p2\] always ring_buffer.count != 17: INCONCLUSIVE$
+^EXIT=10$
+^SIGNAL=0$
diff --git a/regression/ebmc/ring_buffer_induction/ring_buffer.sv b/regression/ebmc/k-induction/ring_buffer.sv
similarity index 70%
rename from regression/ebmc/ring_buffer_induction/ring_buffer.sv
rename to regression/ebmc/k-induction/ring_buffer.sv
index 4bc6482b4..bb7bd68df 100644
--- a/regression/ebmc/ring_buffer_induction/ring_buffer.sv
+++ b/regression/ebmc/k-induction/ring_buffer.sv
@@ -16,13 +16,14 @@ module ring_buffer(input clk, input read, input write);
 
   end
 
-  wire full=count==15;
+  wire full=count==16;
   wire empty=count==0;
 
   assume property (empty |-> !read);
   assume property (full |-> !write);
 
-  assert property (((writeptr-readptr)&'b1111)==count);
+  p0: assert property (((writeptr-readptr)&'b1111)==count[3:0]);
+  p1: assert property (count <= 16);
+  p2: assert property (count != 17);
 
 endmodule
-
diff --git a/regression/ebmc/ring_buffer_induction/test.desc b/regression/ebmc/ring_buffer_induction/test.desc
deleted file mode 100644
index 3047c81e4..000000000
--- a/regression/ebmc/ring_buffer_induction/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-ring_buffer.sv
---k-induction
-^\[ring_buffer\.assert\.1\] assume always \(ring_buffer\.empty |-> !ring_buffer\.read\): ASSUMED$
-^\[ring_buffer\.assert\.2\] assume always \(ring_buffer\.full |-> !ring_buffer\.write\): ASSUMED$
-^\[ring_buffer\.assert\.3\] always \(ring_buffer\.writeptr - ring_buffer\.readptr & 15\) == ring_buffer\.count: PROVED$
-^EXIT=0$
-^SIGNAL=0$