Skip to content

Commit 0677d0a

Browse files
committed
BDD engine: KNOWNBUG for G F properties
Minimal example for a bug in the BDD engine when doing G F properties.
1 parent 0abed59 commit 0677d0a

File tree

2 files changed

+16
-0
lines changed

2 files changed

+16
-0
lines changed

regression/ebmc/BDD/GF1.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
GF1.smv
3+
--bdd
4+
^\[main::spec1\] G F some_var: REFUTED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
Wrong result by BDD engine.

regression/ebmc/BDD/GF1.smv

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
MODULE main
2+
3+
VAR some_var : boolean;
4+
5+
-- should fail
6+
LTLSPEC G F some_var

0 commit comments

Comments
 (0)