6 files changed, 11 insertions, 13 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index e9daa87e..2f04e781 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -42,7 +42,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/st/st.h"
 
diff --git a/src/misc/extra/extraBdd.h b/src/misc/extra/extraBdd.h
index 25df14bb..fcd10320 100644
--- a/src/misc/extra/extraBdd.h
+++ b/src/misc/extra/extraBdd.h
@@ -42,7 +42,6 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
-#include <time.h>
 
 #include "src/misc/st/st.h"
 #include "src/bdd/cudd/cuddInt.h"
diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
index 0416a0d2..08b0f95f 100644
--- a/src/misc/extra/extraBddCas.c
+++ b/src/misc/extra/extraBddCas.c
@@ -192,7 +192,7 @@ Extra_bddEncodingNonStrict(
 {
     DdNode * bEncoded, * bResult;
     int nVarsCol = Cudd_SupportSize(dd,bVarsCol);
-    long clk;
+    clock_t clk;
 
     // cannot work with more that 32-bit codes
     assert( nMulti < 32 );
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index a5f987e3..b54449b4 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1348,9 +1348,9 @@ extraTransferPermuteRecur(
     if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
         return ( Cudd_NotCond( res, comple ) );
 
-    if ( ddS->TimeStop && time(NULL) > ddS->TimeStop )
+    if ( ddS->TimeStop && clock() > ddS->TimeStop )
         return NULL;
-    if ( ddD->TimeStop && time(NULL) > ddD->TimeStop )
+    if ( ddD->TimeStop && clock() > ddD->TimeStop )
         return NULL;
 
     /* Recursive step. */
@@ -1909,9 +1909,9 @@ DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF,
         return bRes;
     Counter++;
 
-    if ( ddF->TimeStop && time(NULL) > ddF->TimeStop )
+    if ( ddF->TimeStop && clock() > ddF->TimeStop )
         return NULL;
-    if ( ddG->TimeStop && time(NULL) > ddG->TimeStop )
+    if ( ddG->TimeStop && clock() > ddG->TimeStop )
         return NULL;
 
     // find the topmost variable in F and G using var order of F
@@ -1982,7 +1982,7 @@ void Extra_TestAndPerm( DdManager * ddF, DdNode * bF, DdNode * bG )
 {
     DdManager * ddG;
     DdNode * bG2, * bRes1, * bRes2;
-    int clk;
+    clock_t clk;
     // disable variable ordering in ddF
     Cudd_AutodynDisable( ddF );
 
diff --git a/src/misc/extra/extraBddTime.c b/src/misc/extra/extraBddTime.c
index 853f8a64..b5e2672a 100644
--- a/src/misc/extra/extraBddTime.c
+++ b/src/misc/extra/extraBddTime.c
@@ -225,7 +225,7 @@ cuddBddAndRecurTime(
     }
 
 //    if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() )
-    if ( TimeOut && time(NULL) > TimeOut )
+    if ( TimeOut && clock() > TimeOut )
         return NULL;
 
     /* Here we can skip the use of cuddI, because the operands are known
@@ -379,7 +379,7 @@ cuddBddAndAbstractRecurTime(
     }
 
 //    if ( TimeOut && ((*pRecCalls)++ % CHECK_FACTOR) == 0 && TimeOut < clock() )
-    if ( TimeOut && time(NULL) > TimeOut )
+    if ( TimeOut && clock() > TimeOut )
         return NULL;
 
     if (topf == top) {
@@ -596,7 +596,7 @@ extraTransferPermuteRecurTime(
     if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
         return ( Cudd_NotCond( res, comple ) );
 
-    if ( TimeOut && time(NULL) > TimeOut )
+    if ( TimeOut && clock() > TimeOut )
         return NULL;
 
     /* Recursive step. */
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index fe8b25f1..7f19480c 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -347,7 +347,7 @@ void (*Extra_UtilMMoutOfMemory)( long size ) = (void (*)( long size ))Extra_Util
   SeeAlso     []
 
 ***********************************************************************/
-long Extra_CpuTime()
+clock_t Extra_CpuTime()
 {
     return clock();
 }
@@ -366,7 +366,7 @@ long Extra_CpuTime()
 #if defined(NT) || defined(NT64) || defined(WIN32)
 double Extra_CpuTimeDouble()
 {
-    return (double)clock()/CLOCKS_PER_SEC;
+    return 1.0*clock()/CLOCKS_PER_SEC;
 }
 #else