Fixed the overflow timeout problem in bmc/bmc2/bmc3/int/pdr/sim, etc.

22 files changed, 78 insertions, 62 deletions

diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 44b917c7..4be740cd 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -611,6 +611,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
     Gia_ManSim_t * p;
     int i, clkTotal = clock();
     int iOut, iPat, RetValue = 0;
+    int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0;
     if ( pAig->pReprs && pAig->pNexts )
         return Gia_ManSimSimulateEquiv( pAig, pPars );
     ABC_FREE( pAig->pCexSeq );
@@ -647,7 +648,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             RetValue = 1;
             break;
         }
-        if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+        if ( time(NULL) > pPars->TimeLimit )
         {
             i++;
             break;
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index e1a5aa07..27945704 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -641,6 +641,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
     Gia_Obj_t * pObj;
     int i, clkTotal = clock();
     int RetValue = 0, iOut, iPat;
+    int nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit + time(NULL) : 0;
     assert( pAig->pReprs && pAig->pNexts );
     ABC_FREE( pAig->pCexSeq );
     p = Gia_Sim2Create( pAig, pPars );
@@ -681,7 +682,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
         }
         if ( pAig->pReprs && pAig->pNexts )
             Gia_Sim2InfoRefineEquivs( p );
-        if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+        if ( time(NULL) > nTimeToStop )
         {
             i++;
             break;
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index d6295931..0cd5eb36 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -81,11 +81,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     Inter_Check_t * pCheck = NULL;
     Aig_Man_t * pAigTemp;
     int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
-    int nTimeNewOut = 0;
-
-    // set runtime limit
-    if ( pPars->nSecLimit )
-        nTimeNewOut = clock() + pPars->nSecLimit * CLOCKS_PER_SEC;
+    int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
 
     // sanity checks
     assert( Saig_ManRegNum(pAig) > 0 );
@@ -252,7 +248,7 @@ p->timeCnf += clock() - clk;
             }
             else if ( RetValue == -1 ) 
             {
-                if ( pPars->nSecLimit && clock() > nTimeNewOut ) // timed out
+                if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out
                 {
                     if ( pPars->fVerbose )
                         printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
@@ -331,7 +327,7 @@ p->timeEqu += clock() - clk - timeTemp;
                 Inter_CheckStop( pCheck );
                 return 1;
             }
-            if ( pPars->nSecLimit && clock() > nTimeNewOut )
+            if ( pPars->nSecLimit && time(NULL) > nTimeNewOut )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
                 p->timeTotal = clock() - clkTotal;
diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c
index 16b62850..e427eb24 100644
--- a/src/aig/llb/llb1Reach.c
+++ b/src/aig/llb/llb1Reach.c
@@ -586,10 +586,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     int nThreshold = 10000;
 
     // compute time to stop
-    if ( p->pPars->TimeLimit )
-        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        p->pPars->TimeTarget = 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
 
     // define variable limits
     Llb_ManPrepareVarLimits( p );
@@ -660,7 +657,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     { 
         clk2 = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 7badc1fb..4ecd1cdf 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -218,7 +218,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
         p->pPars->TimeTarget = 0;
 */
 
-    if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+    if ( time(NULL) > p->pPars->TimeTarget )
     {
         if ( !p->pPars->fSilent )
             printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
@@ -286,7 +286,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     { 
         clk2 = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -729,10 +729,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     int clk = clock();
 
     // compute time to stop
-    if ( pPars->TimeLimit )
-        pPars->TimeTarget = clock() + pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        pPars->TimeTarget = 0;
+    pPars->TimeTarget = pPars->TimeLimit ? time(NULL) + pPars->TimeLimit : 0;
 
     p = Aig_ManDupFlopsOnly( pAig );
 //Aig_ManShow( p, 0, NULL );
@@ -744,7 +741,7 @@ int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
 
     vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
 
-    if ( pPars->TimeLimit && clock() >= pPars->TimeTarget )
+    if ( pPars->TimeLimit && time(NULL) > pPars->TimeTarget )
     {
         if ( !pPars->fSilent )
             printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index f41e0f6e..e20a1541 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -433,10 +433,8 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
     // compute time to stop
-    if ( p->pPars->TimeLimit )
-        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        p->pPars->TimeTarget = 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+
     // set the stop time parameter
     p->dd->TimeStop  = p->pPars->TimeTarget;
     p->ddG->TimeStop = p->pPars->TimeTarget;
@@ -474,7 +472,7 @@ int Llb_NonlinReachability( Llb_Mnn_t * p )
     { 
         // check the runtime limit
         clk2 = clock();
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 8d096b20..24cd0ac5 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -725,7 +725,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
     { 
         clkIter = clock();
         // check the runtime limit
-        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        if ( p->pPars->TimeLimit && time(NULL) > p->pPars->TimeTarget )
         {
             if ( !p->pPars->fSilent )
                 printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
@@ -929,10 +929,8 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     p->pPars   = pPars;
 
     // compute time to stop
-    if ( p->pPars->TimeLimit )
-        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
-    else
-        p->pPars->TimeTarget = 0;
+    p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
+
     if ( pPars->fCluster )
     {
 //        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index 574371ff..a42515f3 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -254,6 +254,7 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nF
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
     Aig_Obj_t * pObj;
+    int nTimeToStop = time(NULL) + TimeLimit;
     int nCoreLits, * pCoreLits;
     int i, iVar, RetValue, clk;
 if ( fVerbose )
@@ -295,7 +296,7 @@ Abc_PrintTime( 1, "Preparing", clock() - clk );
 
     // set runtime limit
     if ( TimeLimit )
-        sat_solver_set_runtime_limit( pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+        sat_solver_set_runtime_limit( pSat, nTimeToStop );
 
     // run SAT solver
 clk = clock();
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 1fc5a11a..8d9f4ac8 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -750,6 +750,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     Saig_Bmc_t * p;
     Aig_Man_t * pNew;
     Cnf_Dat_t * pCnf;
+    int nTimeToStop = time(NULL) + nTimeOut;
     int nOutsSolved = 0;
     int Iter, RetValue = -1, clk = clock(), clk2, clkTotal = clock();
     int Status = -1;
@@ -769,7 +770,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     } 
     // set runtime limit
     if ( nTimeOut )
-        sat_solver_set_runtime_limit( p->pSat, clock() + nTimeOut * CLOCKS_PER_SEC );
+        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     for ( Iter = 0; ; Iter++ )
     {
         clk2 = clock();
@@ -800,7 +801,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         if ( RetValue != l_False )
             break;
         // check the timeout
-        if ( nTimeOut && ((float)nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        if ( nTimeOut && time(NULL) > nTimeToStop )
         {
             printf( "Reached timeout (%d seconds).\n",  nTimeOut );
             if ( piFrames )
@@ -843,10 +844,10 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
             printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
         else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
             printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else if ( nTimeOut == 0 || nTimeOut > clock() )
-            printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        else if ( nTimeOut && time(NULL) > nTimeToStop )
+            printf( "Reached timeout (%d seconds).\n", nTimeOut );
         else
-            printf( "Reached timeout (%d sec).\n", nTimeOut );
+            printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
     }
     Saig_BmcManStop( p );
     return Status;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 7248ed1a..f6ec3e0d 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1102,6 +1102,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
     int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
     int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
+    int nTimeToStop = time(NULL) + pPars->nTimeOut;
     if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
         printf( "Performing BMC with constraints...\n" );
     p = Saig_Bmc3ManStart( pAig );
@@ -1116,7 +1117,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     } 
     // set runtime limit
     if ( p->pPars->nTimeOut )
-        sat_solver_set_runtime_limit( p->pSat, clock() + p->pPars->nTimeOut * CLOCKS_PER_SEC );
+        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     // perform frames
     Aig_ManRandom( 1 );
     Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract );
@@ -1264,7 +1265,7 @@ clkOther += clock() - clk2;
             else 
             {
                 assert( status == l_Undef );
-                if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+                if ( pPars->nTimeOut && time(NULL) > nTimeToStop )
                 {
                     printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                     Saig_Bmc3ManStop( p );
@@ -1280,7 +1281,7 @@ clkOther += clock() - clk2;
                 Saig_Bmc3ManStop( p );
                 return RetValue;
             }
-            if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            if ( pPars->nTimeOut && time(NULL) > nTimeToStop )
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                 Saig_Bmc3ManStop( p );
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index 5c7c76cf..d0fd2db3 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -686,6 +686,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
     Vec_Int_t * vPPiRefine;
     int f, g, r, i, iSatVar, Lit, Entry, RetValue;
     int nConfBef, nConfAft, clk, clkTotal = clock();
+    int nTimeToStop = time(NULL) + TimeLimit;
     assert( Saig_ManPoNum(pAig) == 1 );
 
     if ( nFramesMax == 0 )
@@ -711,7 +712,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
 
     // set runtime limit
     if ( TimeLimit )
-        sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
     // iterate over the timeframes
     for ( f = 0; f < nFramesMax; f++ )
@@ -750,7 +751,7 @@ Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int
                         printf( "== %3d ==", f );
                     else
                         printf( "         " );
-                    if ( TimeLimit && clock() > clkTotal + TimeLimit * CLOCKS_PER_SEC )
+                    if ( TimeLimit && time(NULL) > nTimeToStop )
                         printf( "       SAT solver timed out after %d seconds.\n", TimeLimit );
                     else if ( RetValue != l_False )
                         printf( "       SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index aed78f36..cedf3c9e 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -465,13 +465,30 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
             continue;
         assert( Saig_ObjIsLo(p->pAig, pObj) || Aig_ObjIsNode(pObj) );
         Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), 1 );
-
+/*
+        // add flop inputs with multiple fanouts
+        if ( Saig_ObjIsLo(p->pAig, pObj) )
+        {
+            Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
+            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObjLi)) )
+//            if ( Aig_ObjRefs( Aig_ObjFanin0(pObjLi) ) > 1 )
+                Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObjLi), 1 );
+        }
+        else
+        {
+            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin0(pObj)) )
+                Vec_IntWriteEntry( vResult, Aig_ObjFaninId0(pObj), 1 );
+            if ( !Saig_ObjIsPi(p->pAig, Aig_ObjFanin1(pObj)) )
+                Vec_IntWriteEntry( vResult, Aig_ObjFaninId1(pObj), 1 );
+        }
+*/
         if ( p->vVec2Use )
         {
             iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
             Vec_IntWriteEntry( p->vVec2Use, iVecId * p->nFramesMax + Vec_IntEntry(p->vCla2Fra, ClaId), 1 );
         }
     }
+//    printf( "Number of entries %d\n", Vec_IntCountPositive(vResult) );
 
     // count the number of objects in each frame
     if ( p->vVec2Use )
@@ -508,6 +525,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n
     Aig_Gla2Man_t * p;
     Vec_Int_t * vCore, * vResult;
     int clk, clkTotal = clock();
+    int nTimeToStop = time(NULL) + TimeLimit;
     assert( Saig_ManPoNum(pAig) == 1 );
 
     if ( fVerbose )
@@ -531,7 +549,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n
 
     // set runtime limit
     if ( TimeLimit )
-        sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
+        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
     // compute UNSAT core
     clk = clock();
diff --git a/src/aig/ssw/sswFilter.c b/src/aig/ssw/sswFilter.c
index 8b758915..7298c5f8 100644
--- a/src/aig/ssw/sswFilter.c
+++ b/src/aig/ssw/sswFilter.c
@@ -383,6 +383,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
     Ssw_Pars_t Pars, * pPars = &Pars;
     Ssw_Man_t * p;
     int r, TimeLimitPart, clkTotal = clock();
+    int nTimeToStop = TimeLimit ? TimeLimit + time(NULL) : 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
     // consider the case of empty AIG
@@ -428,7 +429,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
             Ssw_ClassesPrint( p->ppClasses, 0 );
         }
         p->pMSat = Ssw_SatStart( 0 );
-        TimeLimitPart = TimeLimit ? TimeLimit - (int)((float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) : 0;
+        TimeLimitPart = TimeLimit ? nTimeToStop - time(NULL) : 0;
         if ( TimeLimit2 )
         {
             if ( TimeLimitPart )
@@ -443,7 +444,7 @@ void Ssw_SignalFilter( Aig_Man_t * pAig, int nFramesMax, int nConfMax, int nRoun
         // simulate pattern forward
         Ssw_ManRollForward( p, p->pPars->nFramesK );
         // check timeout
-        if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        if ( TimeLimit && time(NULL) > nTimeToStop )
         {
             printf( "Reached timeout (%d seconds).\n",  TimeLimit );
             break;
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index ad37af25..7a676fee 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -895,6 +895,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
     int fMiter = 1;
     Ssw_RarMan_t * p;
     int r, f, clk, clkTotal = clock();
+    int nTimeToStop = time(NULL) + TimeOut;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -933,7 +934,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
                 goto finish;
             }
             // check timeout
-            if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            if ( TimeOut && time(NULL) > nTimeToStop )
             {
                 if ( fVerbose ) printf( "\n" );
                 printf( "Reached timeout (%d seconds).\n",  TimeOut );
@@ -1002,6 +1003,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
 {
     Ssw_RarMan_t * p;
     int r, f, i, k, clkTotal = clock();
+    int nTimeToStop = time(NULL) + TimeOut;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -1071,7 +1073,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
                 goto finish;
             }
             // check timeout
-            if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            if ( TimeOut && time(NULL) > nTimeToStop )
             {
                 if ( fVerbose ) printf( "\n" );
                 printf( "Reached timeout (%d seconds).\n",  TimeOut );
diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c
index 3026cf6b..d8cb9c16 100644
--- a/src/aig/ssw/sswRarity2.c
+++ b/src/aig/ssw/sswRarity2.c
@@ -309,6 +309,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     int fMiter = 1;
     Ssw_RarMan_t * p;
     int r, clk, clkTotal = clock();
+    int nTimeToStop = time(NULL) + TimeOut;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -351,7 +352,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
             printf( "." );
         }
         // check timeout
-        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        if ( TimeOut && time(NULL) > nTimeToStop )
         {
             if ( fVerbose ) printf( "\n" );
             printf( "Reached timeout (%d seconds).\n",  TimeOut );
@@ -386,6 +387,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
     int fMiter = 0;
     Ssw_RarMan_t * p;
     int r, i, k, clkTotal = clock();
+    int nTimeToStop = time(NULL) + TimeOut;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -458,7 +460,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
         Ssw_RarTransferPatterns( p, p->vInits );
         Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
         // check timeout
-        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        if ( TimeOut && time(NULL) > nTimeToStop )
         {
             if ( fVerbose ) printf( "\n" );
             printf( "Reached timeout (%d seconds).\n",  TimeOut );
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 2f38490d..b42f376d 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -259,7 +259,7 @@ cuddBddAndAbstractRecur(
         }
     }
 
-    if ( manager->TimeStop && manager->TimeStop < clock() )
+    if ( manager->TimeStop && manager->TimeStop < time(NULL) )
         return NULL;
 
     if (topf == top) {
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index 4e75aab2..d1afdbee 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -926,7 +926,7 @@ cuddBddAndRecur(
         if (r != NULL) return(r);
     }
 
-    if ( manager->TimeStop && manager->TimeStop < clock() )
+    if ( manager->TimeStop && manager->TimeStop < time(NULL) )
         return NULL;
 
     /* Here we can skip the use of cuddI, because the operands are known
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index 97a6f393..c051666d 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -976,9 +976,9 @@ cuddBddTransferRecur(
     if (st_lookup(table, (const char *)f, (char **)&res))
         return(Cudd_NotCond(res,comple));
 
-    if ( ddS->TimeStop && ddS->TimeStop < clock() )
+    if ( ddS->TimeStop && ddS->TimeStop < time(NULL) )
         return NULL;
-    if ( ddD->TimeStop && ddD->TimeStop < clock() )
+    if ( ddD->TimeStop && ddD->TimeStop < time(NULL) )
         return NULL;
     
     /* Recursive step. */
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index 8dd8f8c5..7c99ac62 100644
--- a/src/bdd/cudd/cuddCompose.c
+++ b/src/bdd/cudd/cuddCompose.c
@@ -1251,7 +1251,7 @@ cuddBddVarMapRecur(
         return(Cudd_NotCond(res,F != f));
     }
 
-    if ( manager->TimeStop && manager->TimeStop < clock() )
+    if ( manager->TimeStop && manager->TimeStop < time(NULL) )
         return NULL;
 
     /* Split and recur on children of this node. */
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index a7ef7845..3386e798 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -367,7 +367,7 @@ cuddSymmSifting(
         if (ddTotalNumberSwapping >= table->siftMaxSwap)
             break;
         // enable timeout during variable reodering - alanmi 2/13/11
-        if ( table->TimeStop && table->TimeStop < clock() )
+        if ( table->TimeStop && table->TimeStop < time(NULL) )
             break;
         x = table->perm[var[i]];
 #ifdef DD_STATS
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index a3da3e30..ac2202dc 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1485,7 +1485,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //        int nConfs = 0;
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
-        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
 
         if (s->verbosity >= 1)
@@ -1510,7 +1510,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 
 //        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
         nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
-
+//printf( "%d ", s->stats.conflicts  );
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
         {
@@ -1523,9 +1523,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
         }
-        if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
     }
+//printf( "\n" );
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index 04caba1e..e3c3781f 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -514,7 +514,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
         }
 
         // check the timeout
-        if ( p->timeToStop && clock() >= p->timeToStop )
+        if ( p->timeToStop && time(NULL) > p->timeToStop )
             return -1;
     }
     return 1;
@@ -538,7 +538,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     int k, RetValue = -1;
     int clkTotal = clock();
     int clkStart = clock();
-    p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut);
+    p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // create the first timeframe
     Pdr_ManCreateSolver( p, (k = 0) );
@@ -619,7 +619,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         }
 
         // check the timeout
-        if ( p->timeToStop && clock() >= p->timeToStop )
+        if ( p->timeToStop && time(NULL) > p->timeToStop )
         {
             if ( fPrintClauses )
             {