diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc
new file mode 100644
index 000000000..9f6f161ed
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+../../verilog/SVA/cycle_delay_star1.sv
+--buechi --bdd
+^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This gives the wrong answer.
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc
new file mode 100644
index 000000000..5ea242c3c
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+../../verilog/SVA/cycle_delay_star1.sv
+--buechi --bound 10
+^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This gives the wrong answer.
diff --git a/regression/ebmc-spot/sva-buechi/disable_iff1.bdd.desc b/regression/ebmc-spot/sva-buechi/disable_iff1.bdd.desc
new file mode 100644
index 000000000..fca389d5d
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/disable_iff1.bdd.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+../../verilog/SVA/disable_iff1.sv
+--buechi --module main --bdd --numbered-trace
+^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED$
+^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED$
+^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^Counterexample with 3 states:$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The trace is missing.
diff --git a/regression/ebmc-spot/sva-buechi/if1.bdd.desc b/regression/ebmc-spot/sva-buechi/if1.bdd.desc
new file mode 100644
index 000000000..c509e0f07
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/if1.bdd.desc
@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/if1.sv
+--buechi --bdd
+^\[main\.p0\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1\): PROVED$
+^\[main\.p1\] always \(if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/issue669.desc b/regression/ebmc-spot/sva-buechi/issue669.desc
new file mode 100644
index 000000000..224238f07
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/issue669.desc
@@ -0,0 +1,17 @@
+CORE
+../../verilog/SVA/issue669.sv
+--buechi --bound 5 --top top
+\[top\.assert\.1\] always not s_eventually 0: PROVED up to bound 5$
+\[top\.assert\.2\] always \(\(top\.a until_with top\.b\) implies \(not \(\(not top\.b\) s_until \(not top\.a\)\)\)\): PROVED up to bound 5$
+\[top\.assert\.3\] always \(\(not \(\(not top\.b\) s_until \(not top\.a\)\)\) implies \(top\.a until_with top\.b\)\): PROVED up to bound 5$
+\[top\.assert\.4\] always \(\(top\.a until_with top\.b\) implies \(top\.a until \(top\.a and top\.b\)\)\): PROVED up to bound 5$
+\[top\.assert\.5\] always \(\(top\.a until \(top\.a and top\.b\)\) implies \(top\.a until_with top\.b\)\): PROVED up to bound 5$
+\[top\.assert\.6\] always \(\(s_eventually top\.a\) implies \(1 s_until top\.a\)\): PROVED up to bound 5$
+\[top\.assert\.7\] always \(\(1 s_until top\.a\) implies \(s_eventually top\.a\)\): PROVED up to bound 5$
+\[top\.assert\.8\] always \(\(top\.a s_until top\.b\) implies \(\(s_eventually top\.b\) and \(top\.a until top\.b\)\)\): PROVED up to bound 5$
+\[top\.assert\.9\] always \(\(\(s_eventually top\.b\) and \(top\.a until top\.b\)\) implies \(top\.a s_until top\.b\)\): PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+https://github.com/diffblue/hw-cbmc/issues/669
diff --git a/regression/ebmc-spot/sva-buechi/s_eventually2.bdd.desc b/regression/ebmc-spot/sva-buechi/s_eventually2.bdd.desc
new file mode 100644
index 000000000..ddcc68d63
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/s_eventually2.bdd.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+../../verilog/SVA/s_eventually2.sv
+--buechi --module main --bdd
+^\[main\.p0\] always s_eventually main.reset \|\| main\.counter == 10: PROVED up to bound 20$
+^\[main\.p1\] always \(s_eventually \[0:2\] main.reset \|\| main\.counter == 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This gives the wrong answer for main.p0.
diff --git a/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc b/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc
new file mode 100644
index 000000000..0503d5490
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+../../verilog/SVA/s_eventually2.sv
+--buechi --module main --bound 20
+^\[main\.p0\] always s_eventually main.reset \|\| main\.counter == 10: PROVED up to bound 20$
+^\[main\.p1\] always \(s_eventually \[0:2\] main.reset \|\| main\.counter == 10\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This gives the wrong answer for main.p0.
diff --git a/regression/ebmc-spot/sva-buechi/s_until1.bdd.desc b/regression/ebmc-spot/sva-buechi/s_until1.bdd.desc
new file mode 100644
index 000000000..613ca7def
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/s_until1.bdd.desc
@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/s_until1.sv
+--buechi --bdd
+^\[.*\] \$past\(main\.counter\) <= main\.counter s_until main\.counter == 10: PROVED$
+^\[.*\] 1 s_until main\.counter == 11: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_and2.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_and2.bmc.desc
new file mode 100644
index 000000000..d233630e4
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_and2.bmc.desc
@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_and2.sv
+--buechi
+\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED up to bound 5$
+\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED up to bound 5$
+\[.*\] \(\(##2 1\) and 1\) #-# main\.x == 2: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition4.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition4.bdd.desc
new file mode 100644
index 000000000..f6427406f
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_repetition4.bdd.desc
@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence_repetition4.sv
+--buechi --bdd
+^\[main\.p0\] \(main\.x == 0 ##1 main\.x == 1\) \[\*2\]: PROVED$
+^\[main\.p1\] \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 0\) \[\*2\]: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_repetition7.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_repetition7.bdd.desc
new file mode 100644
index 000000000..601915034
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_repetition7.bdd.desc
@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/sequence_repetition7.sv
+--buechi --bdd
+^\[.*\] \(main\.a ##1 main\.b\) \[\*5\]: PROVED$
+^\[.*\] \(\!main\.b ##1 \!main\.a\) \[\*5\]: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/ebmc-spot/sva-buechi/sva_abort1.bdd.desc b/regression/ebmc-spot/sva-buechi/sva_abort1.bdd.desc
new file mode 100644
index 000000000..6399d2f4a
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sva_abort1.bdd.desc
@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/sva_abort1.sv
+--buechi --module main --bdd
+^\[main\.p0\] always \(accept_on \(main\.counter == 0\) main\.counter != 0\): PROVED$
+^\[main\.p1\] always \(accept_on \(1\) 0\): PROVED$
+^\[main\.p2\] always \(accept_on \(main\.counter == 1\) main\.counter == 0\): REFUTED$
+^\[main\.p3\] always \(reject_on \(main\.counter != 0\) 1\): REFUTED$
+^\[main\.p4\] always \(reject_on \(1\) 1\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--