diff --git a/NEWS b/NEWS
index ad369269e..edf202962 100644
--- a/NEWS
+++ b/NEWS
@@ -11,6 +11,15 @@ New in spot 1.2.2a (not yet released)
     - randltl had trouble generating formulas when all unary, or
       all binary/n-ary operators were disabled.
     - Fix spurious testsuite failure when using Pandas 0.13.
+    - Add the time spent in child processes when measuring time
+      with the timer class.
+    - Fix determinism of the SAT-based minimization encoding.
+      (It would sometimes produce different equivalent automata,
+      because of a different encoding order.)
+    - A the SAT-based minimization is asked for a 10-state automaton
+      and return a 6-state automaton, do not ask for a 9-state
+      automaton in the next iteration...
+
 
 New in spot 1.2.2 (2014-01-24)
 
diff --git a/src/misc/timer.hh b/src/misc/timer.hh
index daa00a933..04fe73d77 100644
--- a/src/misc/timer.hh
+++ b/src/misc/timer.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -69,8 +69,8 @@ namespace spot
 #ifdef SPOT_HAVE_TIMES
       struct tms tmp;
       times(&tmp);
-      start_.utime = tmp.tms_utime;
-      start_.stime = tmp.tms_stime;
+      start_.utime = tmp.tms_utime + tmp.tms_cutime;
+      start_.stime = tmp.tms_stime + tmp.tms_cstime;
 #else
       start_.utime = clock();
 #endif
@@ -83,8 +83,8 @@ namespace spot
 #ifdef SPOT_HAVE_TIMES
       struct tms tmp;
       times(&tmp);
-      total_.utime += tmp.tms_utime - start_.utime;
-      total_.stime += tmp.tms_stime - start_.stime;
+      total_.utime += tmp.tms_utime + tmp.tms_cutime - start_.utime;
+      total_.stime += tmp.tms_stime + tmp.tms_cstime - start_.stime;
 #else
       total_.utime += clock() - start_.utime;
 #endif