Merge pull request #474 from diffblue/GF1

BDD engine: KNOWNBUG for G F properties
diffblue · May 1, 2024 · 56faf94 · 56faf94
2 parents 42959d8 + 0677d0a
commit 56faf94
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/regression/ebmc/BDD/GF1.desc 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
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_var : boolean;
+
+-- should fail
+LTLSPEC G F some_var