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$
 --
diff --git a/regression/verilog/synthesis/always_comb2.aig.desc b/regression/verilog/synthesis/always_comb2.aig.desc
new file mode 100644
index 000000000..b206358cd
--- /dev/null
+++ b/regression/verilog/synthesis/always_comb2.aig.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+always_comb2.sv
+--aig
+^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED .*$
+^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED .*$
+^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This segfaults.