From 922627f71e62e43c7d475846c2cd83ca8d4bcbea Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 16 Nov 2024 10:37:47 +0000
Subject: [PATCH] add deadend test for BDD engine

---
 regression/ebmc/BDD/deadend1.desc | 12 ++++++++++++
 regression/ebmc/BDD/deadend1.smv  | 20 ++++++++++++++++++++
 2 files changed, 32 insertions(+)
 create mode 100644 regression/ebmc/BDD/deadend1.desc
 create mode 100644 regression/ebmc/BDD/deadend1.smv

diff --git a/regression/ebmc/BDD/deadend1.desc b/regression/ebmc/BDD/deadend1.desc
new file mode 100644
index 000000000..b0f54f9e7
--- /dev/null
+++ b/regression/ebmc/BDD/deadend1.desc
@@ -0,0 +1,12 @@
+CORE
+deadend1.smv
+--bdd
+^\[spec1\] AX FALSE: PROVED$
+^\[spec2\] EX FALSE: PROVED$
+^\[spec3\] AX TRUE: PROVED$
+^\[spec4\] EX TRUE: PROVED
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc/BDD/deadend1.smv b/regression/ebmc/BDD/deadend1.smv
new file mode 100644
index 000000000..3fe7f7170
--- /dev/null
+++ b/regression/ebmc/BDD/deadend1.smv
@@ -0,0 +1,20 @@
+MODULE main
+
+VAR some_var : boolean;
+
+INIT some_var = FALSE
+
+-- the initial state is a deadend state
+TRANS FALSE
+
+-- should pass
+SPEC AX FALSE
+
+-- should pass
+SPEC EX FALSE
+
+-- should pass
+SPEC AX TRUE
+
+-- should pass
+SPEC EX TRUE