diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-07 18:15:08 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-07 18:15:08 -0700 |
| commit | 4760983a461142eacceeed45ddcf5598e6a389a2 (patch) | |
| tree | 87afc6370242742e1571cc42ff7824a9d8ce722f /src/proof | |
| parent | 3aab7245738a69f1dd4d898493d5dabf6596ea61 (diff) | |
| download | abc-4760983a461142eacceeed45ddcf5598e6a389a2.tar.gz abc-4760983a461142eacceeed45ddcf5598e6a389a2.tar.bz2 abc-4760983a461142eacceeed45ddcf5598e6a389a2.zip | |
Fixing time primtouts throughout the code.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecCorr_updated.c | 9 | ||||
| -rw-r--r-- | src/proof/fra/fraInd.c | 3 | ||||
| -rw-r--r-- | src/proof/int/intM114p.c | 3 |
3 files changed, 9 insertions, 6 deletions
diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c index 3bea8dbf..0d441629 100644 --- a/src/proof/cec/cecCorr_updated.c +++ b/src/proof/cec/cecCorr_updated.c @@ -830,9 +830,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ManSim_t * pSim; Gia_Man_t * pSrm; unsigned * pInitState = NULL; - int r, RetValue, clkTotal = clock(); - int clkSat = 0, clkSim = 0, clkSrm = 0; - int clk2, clk = clock(); + int r, RetValue; + clock_t clkTotal = clock(); + clock_t clkSat = 0, clkSim = 0, clkSrm = 0; + clock_t clk2, clk = clock(); ABC_FREE( pAig->pReprs ); ABC_FREE( pAig->pNexts ); if ( Gia_ManRegNum(pAig) == 0 ) @@ -917,7 +918,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) int fChanges = 1; while ( fChanges ) { - int clkBmc = clock(); + clock_t clkBmc = clock(); fChanges = 0; pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); if ( Gia_ManPoNum(pSrm) == 0 ) diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c index 633f8979..0c7134aa 100644 --- a/src/proof/fra/fraInd.c +++ b/src/proof/fra/fraInd.c @@ -590,7 +590,8 @@ clk2 = clock(); // verify implications using simulation if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) { - int Temp, clk = clock(); + int Temp; + clock_t clk = clock(); if ( Temp = Fra_ImpVerifyUsingSimulation( p ) ) printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) ); else diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c index f143dc39..ad1ff61d 100644 --- a/src/proof/int/intM114p.c +++ b/src/proof/int/intM114p.c @@ -394,7 +394,8 @@ int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther { M114p_Solver_t pSat; Vec_Int_t * vMapRoots, * vMapVars; - int clk, status, RetValue; + clock_t clk; + int status, RetValue; assert( p->pInterNew == NULL ); // derive the SAT solver pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter, |