diff --git a/src/tgbatest/ltlcross.test b/src/tgbatest/ltlcross.test
index b8fb882ba..6193dee1f 100755
--- a/src/tgbatest/ltlcross.test
+++ b/src/tgbatest/ltlcross.test
@@ -25,8 +25,16 @@ ltl2tgba=../ltl2tgba
 
 
 (
-# A bug reported by Joachim Klein
-echo 'G(Fa & ((a M b) U ((c U !d) M d)))'
+# Some formulas supplied by Joachim Klein.  The first two were
+# incorrectly translated by ltl_to_tgba_fm(), while the other have
+# shown some bugs in other translators.
+cat <<EOF
+G(Fa & ((a M b) U ((c U !d) M d)))
+XF(p2 R (!Fp1 W p1))
+X p0 || ((X p0) V <>p0)
+p0 xor (p0 W X!p0)
+p0 & (!p0 W Xp0)
+EOF
 # Random formulas
 ../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15
 ) |