From 6f9aeaa38395a72b45fe8382aeba46446e8bf1eb Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 29 Oct 2025 10:52:24 -0700 Subject: [PATCH] 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$ --