Fixing time primtouts throughout the code.

18 files changed, 86 insertions, 55 deletions

diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index ff428fa1..4fa9c07a 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -128,7 +128,8 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
     Ssw_Frm_t * pFrm;
     Ssw_Sat_t * pSat;
     Aig_Obj_t * pObj, * pObjFrame;
-    int status, clkPart, Lit, i, f, RetValue;
+    int status, Lit, i, f, RetValue;
+    clock_t clkPart;
 
     // start managers
     assert( Saig_ManRegNum(pAig) > 0 );
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 581b8aed..28c4947a 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -610,7 +610,8 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
     Ssw_Sml_t * pSml;
     Vec_Ptr_t * vCands;
     Aig_Obj_t * pObj;
-    int i, k, RetValue, clk;
+    int i, k, RetValue;
+    clock_t clk;
 
     // start the classes
     p = Ssw_ClassesStart( pAig );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 82977edb..5459aa72 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -408,7 +408,8 @@ int Ssw_ManSweepBmcConstr_old( Ssw_Man_t * p )
 {
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int i, f, iLits, clk;
+    int i, f, iLits;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -497,7 +498,8 @@ p->timeBmc += clock() - clk;
 int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
 {
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int i, f, iLits, clk;
+    int i, f, iLits;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -618,7 +620,8 @@ int Ssw_ManSweepConstr( Ssw_Man_t * p )
 { 
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
-    int nConstrPairs, clk, i, f, iLits;
+    int nConstrPairs, i, f, iLits;
+    clock_t clk;
 //Ssw_ManPrintPolarity( p->pAig );
 
     // perform speculative reduction
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index c51d421c..b27e7eaf 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -236,7 +236,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
     Aig_Man_t * pAigNew;
     int RetValue, nIter = -1;
-    int clk, clkTotal = clock();
+    clock_t clk, clkTotal = clock();
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
     p->nNodesBeg = Aig_ManNodeNum(p->pAig);
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 617bb40f..760f457a 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -262,7 +262,8 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
 ***********************************************************************/
 int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
 {
-    int RetValue1, RetValue2, clk = clock();
+    int RetValue1, RetValue2;
+    clock_t clk = clock();
     // transfer PI simulation information from storage
 //    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     Ssw_ManSweepTransferDyn( p );
@@ -294,7 +295,8 @@ p->timeSimSat += clock() - clk;
 int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
 {
     Aig_Obj_t * pObj, * pRepr, ** ppClass;
-    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    int i, k, nSize, RetValue1, RetValue2;
+    clock_t clk = clock();
     p->nSimRounds++;
     // transfer PI simulation information from storage
 //    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
@@ -372,7 +374,8 @@ int Ssw_ManSweepDyn( Ssw_Man_t * p )
 { 
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew;
-    int clk, i, f;
+    int i, f;
+    clock_t clk;
 
     // perform speculative reduction
 clk = clock();
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 5f467123..3fff79bb 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -278,7 +278,8 @@ Aig_Obj_t * Ssw_ManSweepBmcFilter_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
 int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
 {
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int f, f1, i, clkTotal = clock();
+    int f, f1, i;
+    clock_t clkTotal = clock();
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
     Saig_ManForEachLo( p->pAig, pObj, i )
@@ -383,7 +384,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;
+    clock_t nTimeToStop = TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
     // consider the case of empty AIG
@@ -429,7 +430,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 ? nTimeToStop - time(NULL) : 0;
+        TimeLimitPart = TimeLimit ? (nTimeToStop - clock()) / CLOCKS_PER_SEC : 0;
         if ( TimeLimit2 )
         {
             if ( TimeLimitPart )
@@ -444,7 +445,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 && time(NULL) > nTimeToStop )
+        if ( TimeLimit && clock() > nTimeToStop )
         {
             printf( "Reached timeout (%d seconds).\n",  TimeLimit );
             break;
diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h
index acd273fd..8749cec1 100644
--- a/src/proof/ssw/sswInt.h
+++ b/src/proof/ssw/sswInt.h
@@ -127,16 +127,16 @@ struct Ssw_Man_t_
     int              nRegsBegC;
     int              nRegsEndC;
     // runtime stats
-    int              timeBmc;        // bounded model checking
-    int              timeReduce;     // speculative reduction
-    int              timeMarkCones;  // marking the cones not to be refined
-    int              timeSimSat;     // simulation of the counter-examples
-    int              timeSat;        // solving SAT
-    int              timeSatSat;     // sat
-    int              timeSatUnsat;   // unsat
-    int              timeSatUndec;   // undecided
-    int              timeOther;      // other runtime
-    int              timeTotal;      // total runtime
+    clock_t          timeBmc;        // bounded model checking
+    clock_t          timeReduce;     // speculative reduction
+    clock_t          timeMarkCones;  // marking the cones not to be refined
+    clock_t          timeSimSat;     // simulation of the counter-examples
+    clock_t          timeSat;        // solving SAT
+    clock_t          timeSatSat;     // sat
+    clock_t          timeSatUnsat;   // unsat
+    clock_t          timeSatUndec;   // undecided
+    clock_t          timeOther;      // other runtime
+    clock_t          timeTotal;      // total runtime
 };
 
 // internal SAT manager
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index 8f54432d..97e9cf54 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -479,7 +479,8 @@ int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPai
 {
     Ssw_Pars_t Pars;
     Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     // derive parameters if not given
     if ( pPars == NULL )
         Ssw_ManSetDefaultParams( pPars = &Pars );
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index 71f148e3..e58e9b50 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -77,7 +77,8 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
 ***********************************************************************/
 int Ssw_ManSweepResimulate( Ssw_Man_t * p )
 {
-    int RetValue1, RetValue2, clk = clock();
+    int RetValue1, RetValue2;
+    clock_t clk = clock();
     // transfer PI simulation information from storage
     Ssw_ManSweepTransfer( p );
     // simulate internal nodes
@@ -159,7 +160,8 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
 void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
     assert( Aig_ObjIsCi(pObj) );
     assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
     // check if it makes sense to skip some calls
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index e356aa60..e4228685 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -320,7 +320,8 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
     Ssw_Pars_t Pars, * pPars = &Pars;
     Vec_Int_t * vIds1, * vIds2;
     Aig_Obj_t * pObj, * pRepr;
-    int RetValue, i, clk = clock();
+    int RetValue, i;
+    clock_t clk = clock();
     Ssw_ManSetDefaultParams( pPars );
     pPars->fVerbose = 1;
     pAigNew = Ssw_SignalCorrespondence( pAig, pPars );
@@ -379,7 +380,8 @@ Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig )
 int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     assert( vIds1 != NULL && vIds2 != NULL );
     // try the new AIGs
     printf( "Performing specialized verification with node pairs.\n" );
@@ -413,7 +415,8 @@ int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, V
 int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes, * pMiter;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     // try the new AIGs
     printf( "Performing general verification without node pairs.\n" );
     pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
@@ -449,7 +452,8 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
 int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars )
 {
     Aig_Man_t * pAigRes;
-    int RetValue, clk = clock();
+    int RetValue;
+    clock_t clk = clock();
     // try the new AIGs
 //    printf( "Performing general verification without node pairs.\n" );
     pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index 5a3aea10..22340779 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -53,7 +53,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     int * pMapBack;
     int i, nCountPis, nCountRegs;
     int nClasses, nPartSize, fVerbose;
-    int clk = clock();
+    clock_t clk = clock();
     if ( pPars->fConstrs )
     {
         printf( "Cannot use partitioned computation with constraints.\n" );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 032bc5ba..7048927f 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -286,7 +286,8 @@ void transpose64Simple( word A[64], word B[64] )
 void TransposeTest()
 {
     word M[64], N[64];
-    int i, clk;
+    int i;
+    clock_t clk;
     Aig_ManRandom64( 1 );
 //    for ( i = 0; i < 64; i++ )
 //        M[i] = Aig_ManRandom64( 0 );
@@ -896,8 +897,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
     int fTryBmc = 0;
     int fMiter = 1;
     Ssw_RarMan_t * p;
-    int r, f = -1, clk, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeOut;
+    int r, f = -1;
+    clock_t clk, clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     int iFrameFail = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
@@ -945,7 +947,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
                 goto finish;
             }
             // check timeout
-            if ( TimeOut && time(NULL) > nTimeToStop )
+            if ( TimeOut && clock() > nTimeToStop )
             {
                 if ( fVerbose ) printf( "\n" );
                 printf( "Reached timeout (%d seconds).\n",  TimeOut );
@@ -1013,8 +1015,9 @@ int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, in
 int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
     Ssw_RarMan_t * p;
-    int r, f = -1, i, k, clkTotal = clock();
-    int nTimeToStop = time(NULL) + TimeOut;
+    int r, f = -1, i, k;
+    clock_t clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -1084,7 +1087,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
                 goto finish;
             }
             // check timeout
-            if ( TimeOut && time(NULL) > nTimeToStop )
+            if ( TimeOut && clock() > nTimeToStop )
             {
                 if ( fVerbose ) printf( "\n" );
                 printf( "Reached timeout (%d seconds).\n",  TimeOut );
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index 0851cf3d..1d93de60 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -308,8 +308,9 @@ 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 r;
+    clock_t clk, clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -352,7 +353,7 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
             printf( "." );
         }
         // check timeout
-        if ( TimeOut && time(NULL) > nTimeToStop )
+        if ( TimeOut && clock() > nTimeToStop )
         {
             if ( fVerbose ) printf( "\n" );
             printf( "Reached timeout (%d seconds).\n",  TimeOut );
@@ -386,8 +387,9 @@ 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 r, i, k;
+    clock_t clkTotal = clock();
+    clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -460,7 +462,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 && time(NULL) > nTimeToStop )
+        if ( TimeOut && clock() > nTimeToStop )
         {
             if ( fVerbose ) printf( "\n" );
             printf( "Reached timeout (%d seconds).\n",  TimeOut );
diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c
index 7d371cac..e5971a64 100644
--- a/src/proof/ssw/sswSat.c
+++ b/src/proof/ssw/sswSat.c
@@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START
 int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
-    int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
+    int pLits[3], nLits, RetValue, RetValue1;
+    clock_t clk;//, status;
     p->nSatCalls++;
     p->pMSat->nSolverCalls++;
 
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index a04f6f54..e58ba848 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -179,7 +179,8 @@ int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
     Ssw_Man_t * p = pBmc->pMan;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
     unsigned * pInfo;
-    int i, f, clk, RetValue, fFirst = 0;
+    int i, f, RetValue, fFirst = 0;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -260,7 +261,8 @@ p->timeBmc += clock() - clk;
 int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
 {
     Ssw_Sem_t * p;
-    int RetValue, Frames, Iter, clk = clock();
+    int RetValue, Frames, Iter;
+    clock_t clk = clock();
     p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
     if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
     {
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index b53e8baf..bb4a55d2 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -38,7 +38,7 @@ struct Ssw_Sml_t_
     int              nWordsPref;        // the number of word in the prefix
     int              fNonConstOut;      // have seen a non-const-0 output during simulation
     int              nSimRounds;        // statistics
-    int              timeSim;           // statistics
+    clock_t          timeSim;           // statistics
     unsigned         pData[0];          // simulation data for the nodes
 };
 
@@ -1005,7 +1005,8 @@ int Ssw_SmlCheckNonConstOutputs( Ssw_Sml_t * p )
 void Ssw_SmlSimulateOne( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int f, i, clk;
+    int f, i;
+    clock_t clk;
 clk = clock();
     for ( f = 0; f < p->nFrames; f++ )
     {
@@ -1116,7 +1117,8 @@ void Ssw_SmlSimulateOneDyn_rec( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f, int * pV
 void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, clk;
+    int i;
+    clock_t clk;
 clk = clock();
     // simulate the nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 098b1e0f..4d1b3ba2 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -45,7 +45,8 @@ ABC_NAMESPACE_IMPL_START
 void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
 {
     Aig_Obj_t * pObj;
-    int i, RetValue1, RetValue2, clk = clock();
+    int i, RetValue1, RetValue2;
+    clock_t clk = clock();
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
     Aig_ManForEachCi( p->pAig, pObj, i )
@@ -90,7 +91,8 @@ p->timeSimSat += clock() - clk;
 ***********************************************************************/
 void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
 {
-    int RetValue1, RetValue2, clk = clock();
+    int RetValue1, RetValue2;
+    clock_t clk = clock();
     // set the PI simulation information
     Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     // simulate internal nodes
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index 5dd7a1f2..ab6952a2 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -187,7 +187,8 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
 int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
-    int RetValue, clk;
+    int RetValue;
+    clock_t clk;
     // get representative of this class
     pObjRepr = Aig_ObjRepr( p->pAig, pObj );
     if ( pObjRepr == NULL )
@@ -267,7 +268,8 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p )
 {
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
-    int i, f, clk;
+    int i, f;
+    clock_t clk;
 clk = clock();
 
     // start initialized timeframes
@@ -365,7 +367,8 @@ int Ssw_ManSweep( Ssw_Man_t * p )
     static int Counter;
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
-    int nConstrPairs, clk, i, f;
+    int nConstrPairs, i, f;
+    clock_t clk;
     Vec_Int_t * vDisproved;
 
     // perform speculative reduction