BDD: add AF AG dead-end reproducer

Add a minimal KNOWNBUG regression that isolates the remaining AF AG dead-end behavior in the BDD CTL engine.

The model has one state that can self-loop forever or branch once into a dead-end bad state. The current BDD implementation refutes AF AG good on that model.

Author: kroening

regression/ebmc/BDD/AFAG_deadend1.desc

@@ -0,0 +1,14 @@
+KNOWNBUG
+AFAG_deadend1.smv
+--bdd
+^\[spec1\] AF AG good: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BDD implementation of nested AG uses AG p = !EF !p over the raw
+transition relation. A finite branch into a deadend state with !p is therefore
+treated as a witness against AG p, even though the existing deadend regressions
+use conventions where finite deadend branches do not falsify universal
+properties.

regression/ebmc/BDD/AFAG_deadend1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR good : boolean;
+
+INIT good = TRUE
+
+TRANS good & next(good) | good & !next(good)
+
+-- There is an infinite path that stays in good forever and a finite path to a
+-- deadend state with good = FALSE. Under the deadend conventions used by the
+-- existing BDD regressions, the finite branch should not falsify AG good.
+SPEC AF AG good