2 files changed, 20 insertions, 3 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index dc2aac28..8f86fc32 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -607,6 +607,7 @@ extern unsigned    Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux
 
 
 extern long        Extra_CpuTime();
+extern double      Extra_CpuTimeDouble();
 extern int         Extra_GetSoftDataLimit();
 extern void        Extra_UtilGetoptReset();
 extern int         Extra_UtilGetopt( int argc, char *argv[], char *optstring );
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index e2c407cd..abe08d7a 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -344,20 +344,36 @@ void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory;
   SeeAlso     []
 
 ***********************************************************************/
-#if defined(NT) || defined(NT64) || defined(WIN32)
 long Extra_CpuTime()
 {
     return clock();
 }
+
+/**Function*************************************************************
+
+  Synopsis    [util_cpu_time()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#if defined(NT) || defined(NT64) || defined(WIN32)
+double Extra_CpuTimeDouble()
+{
+    return (double)clock()/CLOCKS_PER_SEC;
+}
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
-long Extra_CpuTime()
+double Extra_CpuTimeDouble()
 {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
-    return (long)(CLOCKS_PER_SEC * ((double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000)); 
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; 
 }
 #endif