diff --git a/regression/ebmc/Makefile b/regression/ebmc/Makefile
index 68b2eefbf..e1fd1086f 100644
--- a/regression/ebmc/Makefile
+++ b/regression/ebmc/Makefile
@@ -3,7 +3,10 @@ default: test
 TEST_PL = ../../lib/cbmc/regression/test.pl
 
 test:
-	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc
+	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc -X buechi
+
+test-buechi:
+	@$(TEST_PL) -e -p -c ../../../src/ebmc/ebmc -I buechi
 
 test-z3:
-	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend
+	@$(TEST_PL) -e -p -c "../../../src/ebmc/ebmc --z3" -X broken-smt-backend -X buechi
diff --git a/regression/ebmc/queues/queue_depth1.desc b/regression/ebmc/queues/queue_depth1.desc
new file mode 100644
index 000000000..210907e03
--- /dev/null
+++ b/regression/ebmc/queues/queue_depth1.desc
@@ -0,0 +1,8 @@
+CORE buechi
+queue_depth1.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/queues/queue_depth1.sv b/regression/ebmc/queues/queue_depth1.sv
new file mode 100644
index 000000000..b6f999799
--- /dev/null
+++ b/regression/ebmc/queues/queue_depth1.sv
@@ -0,0 +1,19 @@
+module queue(
+  input in_data, in_valid,
+  output out_data, out_valid,
+  input clk);
+
+  reg data;
+  reg valid;
+
+  initial valid = 0;
+
+  always_ff @(posedge clk)
+    {data, valid} <= {in_data, in_valid};
+
+  assign out_data = data;
+  assign out_valid = valid;
+
+  assert property (@(posedge clk) in_valid implies s_eventually out_valid);
+
+endmodule
diff --git a/regression/ebmc/queues/queue_depth2.desc b/regression/ebmc/queues/queue_depth2.desc
new file mode 100644
index 000000000..b4f6d89e0
--- /dev/null
+++ b/regression/ebmc/queues/queue_depth2.desc
@@ -0,0 +1,8 @@
+CORE buechi
+queue_depth2.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/queues/queue_depth2.sv b/regression/ebmc/queues/queue_depth2.sv
new file mode 100644
index 000000000..1caa78f39
--- /dev/null
+++ b/regression/ebmc/queues/queue_depth2.sv
@@ -0,0 +1,21 @@
+module queue(
+  input in_data, in_valid,
+  output out_data, out_valid,
+  input clk);
+
+  reg data0, data1;
+  reg valid0, valid1;
+
+  initial {valid0, valid1} = 2'b00;
+
+  always_ff @(posedge clk) begin
+    {data0, valid0} <= {in_data, in_valid};
+    {data1, valid1} <= {data0, valid0};
+  end
+
+  assign out_data = data1;
+  assign out_valid = valid1;
+
+  assert property (@(posedge clk) in_valid implies s_eventually out_valid);
+
+endmodule
diff --git a/regression/ebmc/queues/queue_depthN.desc b/regression/ebmc/queues/queue_depthN.desc
new file mode 100644
index 000000000..224fabe11
--- /dev/null
+++ b/regression/ebmc/queues/queue_depthN.desc
@@ -0,0 +1,8 @@
+CORE buechi
+queue_depthN.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/queues/queue_depthN.sv b/regression/ebmc/queues/queue_depthN.sv
new file mode 100644
index 000000000..7b8957a28
--- /dev/null
+++ b/regression/ebmc/queues/queue_depthN.sv
@@ -0,0 +1,24 @@
+module queue
+  #(parameter N = 10)
+  (input in_data, in_valid,
+  output out_data, out_valid,
+  input clk);
+
+  reg [N-1:0] data;
+  reg [N-1:0] valid;
+
+  initial valid = {N{1'b0}};
+
+  always_ff @(posedge clk)
+    {data[0], valid[0]} <= {in_data, in_valid};
+
+  always_ff @(posedge clk)
+    for(integer i=1; i<N; i++)
+      {data[i], valid[i]} <= {data[i-1], valid[i-1]};
+
+  assign out_data = data[N-1];
+  assign out_valid = valid[N-1];
+
+  assert property (@(posedge clk) in_valid implies s_eventually out_valid);
+
+endmodule
diff --git a/regression/ebmc/queues/queue_with_simple_stallN.desc b/regression/ebmc/queues/queue_with_simple_stallN.desc
new file mode 100644
index 000000000..840fba8cf
--- /dev/null
+++ b/regression/ebmc/queues/queue_with_simple_stallN.desc
@@ -0,0 +1,8 @@
+CORE buechi
+queue_with_simple_stallN.sv
+--bdd --buechi
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/queues/queue_with_simple_stallN.sv b/regression/ebmc/queues/queue_with_simple_stallN.sv
new file mode 100644
index 000000000..a9f2f96c5
--- /dev/null
+++ b/regression/ebmc/queues/queue_with_simple_stallN.sv
@@ -0,0 +1,30 @@
+module queue
+  #(parameter N = 10)
+  (input in_data, in_valid, in_stall,
+  output out_data, out_valid, out_stall,
+  input clk);
+
+  reg [N-1:0] data;
+  reg [N-1:0] valid;
+
+  initial valid = {N{1'b0}};
+
+  always_ff @(posedge clk)
+    if(!out_stall)
+      {data[0], valid[0]} <= {in_data, in_valid};
+
+  always_ff @(posedge clk)
+    for(integer i=1; i<N; i++)
+      if(!out_stall)
+        {data[i], valid[i]} <= {data[i-1], valid[i-1]};
+
+  assign out_data = data[N-1];
+  assign out_valid = valid[N-1];
+  assign out_stall = in_stall;
+
+  // we need to assume we are not stalled indefinitively
+  assume property (@(posedge clk) s_eventually !in_stall);
+
+  assert property (@(posedge clk) (in_valid && !out_stall) implies s_eventually out_valid);
+
+endmodule