diff --git a/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc
index 9014dd8a6..c8f1429e8 100644
--- a/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc
+++ b/regression/ebmc-spot/sva-buechi/sequence3.bmc.desc
@@ -1,10 +1,10 @@
 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$
+^\[main\.p0\] strong\(##\[\*\] main\.x == 6\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p1\] strong\(##\[\*\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p2\] strong\(##\[\+\] main\.x == 0\): UNSUPPORTED: sva_strong not convertible to Buechi$
+^\[main\.p3\] strong\(##\[\+\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc
index b0715f719..5318a533f 100644
--- a/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc
+++ b/regression/ebmc-spot/sva-buechi/system_verilog_assertion4.desc
@@ -1,7 +1,7 @@
 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$
+^\[main\.p11\] always \(main\.x == 0 \|-> \(\(##1 main\.x == 1\) and \(not \(##2 main\.x == 3\)\)\)\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
 ^EXIT=10$
 ^SIGNAL=0$
 --