From 6f9aeaa38395a72b45fe8382aeba46446e8bf1eb Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 29 Oct 2025 10:52:24 -0700
Subject: [PATCH 1/2] Repair CI race between #1363 and #1368

This applies the changes needed for #1368 to #1363.
---
 regression/ebmc-spot/sva-buechi/sequence3.bmc.desc        | 8 ++++----
 .../ebmc-spot/sva-buechi/system_verilog_assertion4.desc   | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

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$
 --

From 881fb84ccf10aa18d0724685adb239a230c7a999 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 29 Oct 2025 10:26:01 -0700
Subject: [PATCH 2/2] KNOWNBUG test for Verilog->AIG conversion

---
 regression/verilog/synthesis/always_comb2.aig.desc | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 regression/verilog/synthesis/always_comb2.aig.desc

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.