diff --git a/lib/gethrxtime.h b/lib/gethrxtime.h
index f09ef39c3..9453d609e 100644
--- a/lib/gethrxtime.h
+++ b/lib/gethrxtime.h
@@ -22,6 +22,10 @@
 
 # include "xtime.h"
 
+#ifdef  __cplusplus
+extern "C" {
+#endif
+
 /* Get the current time, as a count of the number of nanoseconds since
    an arbitrary epoch (e.g., the system boot time).  Prefer a
    high-resolution clock that is not subject to resetting or
@@ -34,4 +38,8 @@ static inline xtime_t gethrxtime (void) { return gethrtime (); }
 xtime_t gethrxtime (void);
 # endif
 
+#ifdef  __cplusplus
+}
+#endif
+
 #endif
diff --git a/lib/xtime.h b/lib/xtime.h
index adab518b1..3d235faba 100644
--- a/lib/xtime.h
+++ b/lib/xtime.h
@@ -37,6 +37,10 @@ typedef long int xtime_t;
 #  endif
 # endif
 
+#ifdef  __cplusplus
+extern "C" {
+#endif
+
 /* Return an extended time value that contains S seconds and NS
    nanoseconds, without any overflow checking.  */
 static inline xtime_t
@@ -83,4 +87,8 @@ xtime_nsec (xtime_t t)
   return ns;
 }
 
+#ifdef  __cplusplus
+}
+#endif
+
 #endif
diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am
index c0e3c94da..9b48207a6 100644
--- a/src/bin/Makefile.am
+++ b/src/bin/Makefile.am
@@ -49,3 +49,4 @@ randltl_SOURCES = randltl.cc
 ltl2tgba_SOURCES = ltl2tgba.cc
 ltl2tgta_SOURCES = ltl2tgta.cc
 ltlcheck_SOURCES = ltlcheck.cc
+ltlcheck_LDADD = $(LDADD) $(LIB_GETHRXTIME)
diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcheck.cc
index 2bbc574f9..1954a96c6 100644
--- a/src/bin/ltlcheck.cc
+++ b/src/bin/ltlcheck.cc
@@ -28,7 +28,7 @@
 #include <cstdio>
 #include <argp.h>
 #include "error.h"
-#include <sstream>
+#include "gethrxtime.h"
 
 #include "common_setup.hh"
 #include "common_cout.hh"
@@ -113,6 +113,7 @@ struct statistics
   unsigned scc;
   unsigned nondetstates;
   bool nondeterministic;
+  double time;
   unsigned product_states;
   unsigned product_transitions;
   unsigned product_scc;
@@ -127,6 +128,7 @@ struct statistics
 	   "    \"scc\",\n"
 	   "    \"nondetstates\",\n"
 	   "    \"nondeterministic\",\n"
+	   "    \"time\",\n"
 	   "    \"product_states\",\n"
 	   "    \"product_transitions\",\n"
 	   "    \"product_scc\"");
@@ -142,6 +144,7 @@ struct statistics
        << scc << ", "
        << nondetstates << ", "
        << nondeterministic << ", "
+       << time << ", "
        << product_states << ", "
        << product_transitions << ", "
        << product_scc;
@@ -365,7 +368,9 @@ namespace
       std::string cmd = command.str();
       std::cerr << "Running [" << l << translator_num << "]: "
 		<< cmd << std::endl;
+      xtime_t before = gethrxtime();
       int es = system(cmd.c_str());
+      xtime_t after = gethrxtime();
 
       const spot::tgba* res = 0;
       if (es)
@@ -429,6 +434,8 @@ namespace
 	  st->scc = m.scc_count();
 	  st->nondetstates = spot::count_nondet_states(res);
 	  st->nondeterministic = st->nondetstates != 0;
+          double prec = XTIME_PRECISION;
+	  st->time = (after - before) / prec;
 	}
       return res;
     }