diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index e99fb03e4..cf3ac3cf8 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -175,10 +175,12 @@ jobs:
           DEBIAN_FRONTEND: noninteractive
         run: |
           # spot
-          wget -q -O - https://www.lrde.epita.fr/repo/debian.gpg | sudo apt-key add -
-          sudo sh -c 'echo "deb http://www.lrde.epita.fr/repo/debian/ stable/" >> /etc/apt/sources.list'
-          sudo apt-get update
-          sudo apt-get install spot
+          SPOT_VERSION=2.14.1
+          wget https://www.lre.epita.fr/repo/debian/stable/libbddx0_${SPOT_VERSION}.0-1_amd64.deb
+          wget https://www.lre.epita.fr/repo/debian/stable/libspotgen0_${SPOT_VERSION}.0-1_amd64.deb
+          wget https://www.lre.epita.fr/repo/debian/stable/libspot0_${SPOT_VERSION}.0-1_amd64.deb
+          wget https://www.lre.epita.fr/repo/debian/stable/spot_${SPOT_VERSION}.0-1_amd64.deb
+          sudo dpkg -i libbddx0_${SPOT_VERSION}.0-1_amd64.deb libspotgen0_${SPOT_VERSION}.0-1_amd64.deb libspot0_${SPOT_VERSION}.0-1_amd64.deb spot_${SPOT_VERSION}.0-1_amd64.deb
       - name: Confirm ltl2tgba is available and log the version installed
         run: ltl2tgba --version
       - name: Get the ebmc binary
diff --git a/regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc
new file mode 100644
index 000000000..6995d8f94
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_and2.bdd.desc
@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sequence_and2.sv
+--buechi --bdd
+\[.*\] \(1 and \(##2 1\)\) \|-> main\.x == 2: PROVED$
+\[.*\] \(\(##2 1\) and 1\) \|-> main\.x == 2: PROVED$
+\[.*\] \(\(##2 1\) and 1\) #-# main\.x == 2: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc
new file mode 100644
index 000000000..f53b4b91d
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_or1.bdd.desc
@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/sequence_or1.sv
+--buechi --bdd
+^\[main\.p0\] main\.x == 0 or main\.x == 1: PROVED$
+^\[main\.p1\] strong\(main\.x == 0 or main\.x == 1\): PROVED$
+^\[main\.p2\] main\.x == 0 or \(nexttime main\.x == 1\): PROVED$
+^\[main\.p3\] \(nexttime main\.x == 1\) or main\.x == 1: PROVED$
+^\[main\.p4\] \(main\.x == 0 or main\.x != 10\) |=> main\.x == 1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/regression/verilog/SVA/sequence_and2.sv b/regression/verilog/SVA/sequence_and2.sv
index f6fb0d467..0ea6fc80f 100644
--- a/regression/verilog/SVA/sequence_and2.sv
+++ b/regression/verilog/SVA/sequence_and2.sv
@@ -1,6 +1,6 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   always @(posedge clk)
     x<=x+1;
diff --git a/regression/verilog/SVA/sequence_or1.sv b/regression/verilog/SVA/sequence_or1.sv
index 5f73ac511..9f5cb427a 100644
--- a/regression/verilog/SVA/sequence_or1.sv
+++ b/regression/verilog/SVA/sequence_or1.sv
@@ -1,6 +1,6 @@
 module main(input clk);
 
-  reg [31:0] x = 0;
+  reg [7:0] x = 0;
 
   always @(posedge clk)
     x<=x+1;