KNOWNBUG test for Buechi instrumentation

This reproduces a problem where our numbering for atomic propositions
differs from Spot's.

Author: kroening

regression/ebmc-spot/ltl-buechi/implies3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+implies3.smv
+--buechi --bound 5
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This fails since Spot uses a different atom numbering than we do.

regression/ebmc-spot/ltl-buechi/implies3.smv

@@ -0,0 +1,14 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC ! (F x = 1 -> F x = 0) -- should pass