Merge pull request #817 from diffblue/deadend1

add deadend test for BDD engine

Author: tautschnig

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
+--

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