From 0677d0a2b3057f101bc7c4c92f65da340bda29b0 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 30 Apr 2024 21:04:22 -0400
Subject: [PATCH] BDD engine: KNOWNBUG for G F properties

Minimal example for a bug in the BDD engine when doing G F properties.
---
 regression/ebmc/BDD/GF1.desc | 10 ++++++++++
 regression/ebmc/BDD/GF1.smv  |  6 ++++++
 2 files changed, 16 insertions(+)
 create mode 100644 regression/ebmc/BDD/GF1.desc
 create mode 100644 regression/ebmc/BDD/GF1.smv

diff --git a/regression/ebmc/BDD/GF1.desc b/regression/ebmc/BDD/GF1.desc
new file mode 100644
index 000000000..80ae71845
--- /dev/null
+++ b/regression/ebmc/BDD/GF1.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+GF1.smv
+--bdd
+^\[main::spec1\] G F some_var: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Wrong result by BDD engine.
diff --git a/regression/ebmc/BDD/GF1.smv b/regression/ebmc/BDD/GF1.smv
new file mode 100644
index 000000000..371413b14
--- /dev/null
+++ b/regression/ebmc/BDD/GF1.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_var : boolean;
+
+-- should fail
+LTLSPEC G F some_var