From 7a0058b33ed2db28cc86702fbdace7385cb319e1 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 16 Nov 2024 10:41:15 +0000
Subject: [PATCH] BMC: KNOWNBUG test for AXp

---
 regression/ebmc/BMC/AX1.desc | 11 +++++++++++
 regression/ebmc/BMC/AX1.smv  | 11 +++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 regression/ebmc/BMC/AX1.desc
 create mode 100644 regression/ebmc/BMC/AX1.smv

diff --git a/regression/ebmc/BMC/AX1.desc b/regression/ebmc/BMC/AX1.desc
new file mode 100644
index 000000000..d4543cb7c
--- /dev/null
+++ b/regression/ebmc/BMC/AX1.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+AX1.smv
+--bound 2
+^\[spec1\] AX some_var = TRUE: REFUTED$
+^\[spec2\] AX some_var = FALSE: PROVED up to bound 2$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC encoding fails on the temporal operator.
diff --git a/regression/ebmc/BMC/AX1.smv b/regression/ebmc/BMC/AX1.smv
new file mode 100644
index 000000000..a4cb03cbc
--- /dev/null
+++ b/regression/ebmc/BMC/AX1.smv
@@ -0,0 +1,11 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INVAR some_var = FALSE
+
+-- should fail
+SPEC AX some_var = TRUE
+
+-- should pass
+SPEC AX some_var = FALSE