From ced7a28993cddf5df9e9a42f7ef0e26746bf16e9 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 31 Oct 2025 09:51:48 -0700
Subject: [PATCH] KNOWNBUG tests for Buechi instrumentation

These tests reproduce a problem where our numbering for atomic propositions
differs from Spot's.
---
 regression/ebmc-spot/ltl-buechi/implies3.desc      |  9 +++++++++
 regression/ebmc-spot/ltl-buechi/implies3.smv       | 14 ++++++++++++++
 .../ebmc-spot/sva-buechi/sequence_and1.bdd.desc    | 14 ++++++++++++++
 .../ebmc-spot/sva-buechi/sequence_and1.bmc.desc    | 14 ++++++++++++++
 4 files changed, 51 insertions(+)
 create mode 100644 regression/ebmc-spot/ltl-buechi/implies3.desc
 create mode 100644 regression/ebmc-spot/ltl-buechi/implies3.smv
 create mode 100644 regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc
 create mode 100644 regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc

diff --git a/regression/ebmc-spot/ltl-buechi/implies3.desc b/regression/ebmc-spot/ltl-buechi/implies3.desc
new file mode 100644
index 000000000..a0a1977ba
--- /dev/null
+++ b/regression/ebmc-spot/ltl-buechi/implies3.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+implies3.smv
+--buechi --bound 5
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails since Spot uses a different atom numbering than we do.
diff --git a/regression/ebmc-spot/ltl-buechi/implies3.smv b/regression/ebmc-spot/ltl-buechi/implies3.smv
new file mode 100644
index 000000000..f167e032e
--- /dev/null
+++ b/regression/ebmc-spot/ltl-buechi/implies3.smv
@@ -0,0 +1,14 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC ! (F x = 1 -> F x = 0) -- should pass
diff --git a/regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc b/regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc
new file mode 100644
index 000000000..0e4c523c5
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_and1.bdd.desc
@@ -0,0 +1,14 @@
+KNOWNBUG
+../../verilog/SVA/sequence_and1.sv
+--buechi --bdd
+^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
+^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
+^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED$
+^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED$
+^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails since Spot's AP numbering differs.
diff --git a/regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc b/regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc
new file mode 100644
index 000000000..11d2ae8a4
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence_and1.bmc.desc
@@ -0,0 +1,14 @@
+KNOWNBUG
+../../verilog/SVA/sequence_and1.sv
+--buechi
+^\[main\.p0\] main\.x == 0 and main\.x == 1: REFUTED$
+^\[main\.p1\] strong\(main\.x == 0 and main\.x == 1\): REFUTED$
+^\[main\.p2\] main\.x == 0 and \(nexttime main\.x == 1\): PROVED up to bound \d+$
+^\[main\.p3\] \(nexttime main\.x == 1\) and main\.x == 0: PROVED up to bound \d+$
+^\[main\.p4\] \(main\.x == 0 and main\.x != 10\) |=> main\.x == 1: PROVED up to bound \d+$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails since Spot's AP numbering differs.