diff --git a/regression/ebmc-spot/sva-buechi/immediate2.desc b/regression/ebmc-spot/sva-buechi/immediate2.desc
new file mode 100644
index 000000000..195f6a27c
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/immediate2.desc
@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/immediate2.sv
+--buechi
+^\[main\.assume\.1\] assume always 0: ASSUMED$
+^\[main\.assert\.2\] always main\.index < 10: PROVED \(.*\)$
+^\[main\.assert\.3\] always 0: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/immediate3.desc b/regression/ebmc-spot/sva-buechi/immediate3.desc
new file mode 100644
index 000000000..f3a799bf7
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/immediate3.desc
@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/immediate3.sv
+--buechi
+^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED \(.*\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/s_eventually4.desc b/regression/ebmc-spot/sva-buechi/s_eventually4.desc
new file mode 100644
index 000000000..c073188b3
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/s_eventually4.desc
@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/s_eventually4.sv
+--buechi --module main --bound 11
+^\[main\.p0\] always \(\(s_eventually main\.counter == 1\) or \(s_eventually main.counter == 10\)\): PROVED up to bound 11$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc
new file mode 100644
index 000000000..9014dd8a6
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc
@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence3.sv
+--buechi --bound 20 --numbered-trace
+^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: not convertible to Buechi$
+^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition2.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition2.bmc.desc
new file mode 100644
index 000000000..5ab8f8552
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_repetition2.bmc.desc
@@ -0,0 +1,17 @@
+CORE
+../../verilog/SVA/sequence_repetition2.sv
+--buechi --bound 10
+^\[main\.p0\] main\.x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p1\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
+^\[main\.p2\] main\.x == 0 \[\+\]: PROVED up to bound 10$
+^\[main\.p3\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p4\] main\.x == 1 \[\*\]: REFUTED$
+^\[main\.p5\] 0 \[\*\]: REFUTED$
+^\[main\.p6\] main\.x == 1 \[\+\]: REFUTED$
+^\[main\.p7\] \(main\.x == 0 \[\+\]\) #-# main\.x == 1: REFUTED$
+^\[main\.p8\] 0 \[\+\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition3.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition3.bdd.desc
new file mode 100644
index 000000000..3db6808b6
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_repetition3.bdd.desc
@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_repetition3.sv
+--buechi --bdd
+^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED$
+^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED$
+^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion1.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion1.desc
new file mode 100644
index 000000000..5cc37fc40
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/system_verilog_assertion1.desc
@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/system_verilog_assertion1.sv
+--buechi --module main --bound 20 --trace
+^EXIT=10$
+^SIGNAL=0$
+^Counterexample:$
+--
+^warning: ignoring
diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion2.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion2.desc
new file mode 100644
index 000000000..281dd6507
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/system_verilog_assertion2.desc
@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/system_verilog_assertion2.sv
+--buechi --module main --bound 20 --trace
+^EXIT=10$
+^SIGNAL=0$
+^Counterexample:$
+^\[main\.my_label\] .* REFUTED$
+--
+^warning: ignoring
diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc
new file mode 100644
index 000000000..b0715f719
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc
@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/system_verilog_assertion4.sv
+--buechi --module main --bound 10
+^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/ebmc-spot/sva-buechi/weak1.desc b/regression/ebmc-spot/sva-buechi/weak1.desc
new file mode 100644
index 000000000..388b0fe8a
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/weak1.desc
@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/weak1.sv
+--buechi --bound 20
+^\[main\.p0\] weak\(##\[0:9\] main\.x == 100\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--