From 875339fd80ac17d6e952533b015974623096ae53 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 16 Jul 2025 14:41:50 -0700
Subject: [PATCH] KNOWNBUG tests for LTL BMC

---
 regression/smv/LTL/smv_ltlspec_F4.desc | 10 ++++++++++
 regression/smv/LTL/smv_ltlspec_F4.smv  |  6 ++++++
 regression/smv/LTL/smv_ltlspec_F5.desc | 10 ++++++++++
 regression/smv/LTL/smv_ltlspec_F5.smv  |  7 +++++++
 regression/smv/LTL/smv_ltlspec_F6.desc | 10 ++++++++++
 regression/smv/LTL/smv_ltlspec_F6.smv  |  6 ++++++
 6 files changed, 49 insertions(+)
 create mode 100644 regression/smv/LTL/smv_ltlspec_F4.desc
 create mode 100644 regression/smv/LTL/smv_ltlspec_F4.smv
 create mode 100644 regression/smv/LTL/smv_ltlspec_F5.desc
 create mode 100644 regression/smv/LTL/smv_ltlspec_F5.smv
 create mode 100644 regression/smv/LTL/smv_ltlspec_F6.desc
 create mode 100644 regression/smv/LTL/smv_ltlspec_F6.smv

diff --git a/regression/smv/LTL/smv_ltlspec_F4.desc b/regression/smv/LTL/smv_ltlspec_F4.desc
new file mode 100644
index 000000000..33154fd01
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F4.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_F4.smv
+--bound 3
+^\[spec1\] F \(some_input <-> X some_input\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine gives the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_F4.smv b/regression/smv/LTL/smv_ltlspec_F4.smv
new file mode 100644
index 000000000..7f16b5c60
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F4.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_input : boolean;
+
+-- Expected to fail. The input can alternate infinitely often.
+LTLSPEC F (some_input <-> X some_input)
diff --git a/regression/smv/LTL/smv_ltlspec_F5.desc b/regression/smv/LTL/smv_ltlspec_F5.desc
new file mode 100644
index 000000000..952a884b6
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F5.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_F5.smv
+--bound 3 --numbered-trace
+^\[spec1\] F \(!some_input \& X !some_input\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine gives the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_F5.smv b/regression/smv/LTL/smv_ltlspec_F5.smv
new file mode 100644
index 000000000..dd929f90a
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F5.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+VAR some_input : boolean;
+
+-- Expected to fail
+-- The shortest loop is FALSE, FALSE
+LTLSPEC F (!some_input & X !some_input)
diff --git a/regression/smv/LTL/smv_ltlspec_F6.desc b/regression/smv/LTL/smv_ltlspec_F6.desc
new file mode 100644
index 000000000..be862b8bc
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F6.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_F6.smv
+--bound 3 --numbered-trace
+^\[spec1\] F X some_input: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine gives the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_F6.smv b/regression/smv/LTL/smv_ltlspec_F6.smv
new file mode 100644
index 000000000..9ddd851eb
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F6.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_input : boolean;
+
+-- Expected to fail
+LTLSPEC F X some_input