diff --git a/ChangeLog b/ChangeLog
index de0dc5b7a..cdb33c9b7 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2009-11-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* src/tgbatest/ltlcounter.test (run): Only construct small
+	formulae (i.e. n<=2) under valgrind.  The test case is too
+	slow otherwise.
+
 2009-11-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix spurious failure of style.test.
diff --git a/src/tgbatest/ltlcounter.test b/src/tgbatest/ltlcounter.test
index b1fb2df0f..cd2583ec0 100755
--- a/src/tgbatest/ltlcounter.test
+++ b/src/tgbatest/ltlcounter.test
@@ -31,13 +31,15 @@ lcl=$lcdir/LTLcounterLinear.pl
 lcc=$lcdir/LTLcounterCarry.pl
 lccl=$lcdir/LTLcounterCarryLinear.pl
 
+run='run 0'
+
 check_formula()
 {
   # First, check the satisfiability of the formula with Spot
-  run 0 ../ltl2tgba -e -x -f "$1" >/dev/null
+  $run ../ltl2tgba -e -x -f "$1" >/dev/null
   # Also check the satisfiability of the degeneralized formula
-  run 0 ../ltl2tgba -e -D -x -f "$1" >/dev/null
-  run 0 ../ltl2tgba -e -DS -x -f "$1" >/dev/null
+  $run ../ltl2tgba -e -D -x -f "$1" >/dev/null
+  $run ../ltl2tgba -e -DS -x -f "$1" >/dev/null
 }
 
 # Kristin Y. Rozier reported that the formulae with n=10 were badly
@@ -59,4 +61,10 @@ do
   check_formula "$f"
   f=`"$lccl" $i`
   check_formula "$f"
+  
+  # Only run the first two formulae under valgrind, 
+  # it is too slow otherwise.
+  if test $i = 2; then
+     run=:
+  fi
 done