diff --git a/NEWS b/NEWS
index ed911a584..50bbb72ec 100644
--- a/NEWS
+++ b/NEWS
@@ -9,6 +9,8 @@ New in spot 1.0a (not released):
     - "P0.init" is parsed as an atomic even without the double quotes,
       but it was always output with double quotes.  This version will
       not quote this atomic proposition anymore.
+    - tgba_product::transition_annotation() would segfault when
+      called in a product against a Kripke structure.
   * Minor improvements:
     - Four new LTL simplifications rules:
         GF(a|Xb) = GF(a|b)
diff --git a/iface/dve2/finite.test b/iface/dve2/finite.test
index 26cfceed3..4ab199ec8 100755
--- a/iface/dve2/finite.test
+++ b/iface/dve2/finite.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2011 Laboratoire de Recherche et Développement
+# Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -51,3 +51,7 @@ run 0 ../dve2check -ddead -E $srcdir/finite.dve \
 
 run 0 ../dve2check -ddead -e $srcdir/finite.dve \
   '!(G(dead -> ("P.a==2" | "P.b==3")))'
+
+# This used to segfault because of a bug in
+# tgba_product::transition_annotation.
+run 0 ../dve2check -gp $srcdir/finite.dve true