summaryrefslogtreecommitdiffstats
path: root/src/proof/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssw')
-rw-r--r--src/proof/ssw/sswBmc.c3
-rw-r--r--src/proof/ssw/sswClass.c3
-rw-r--r--src/proof/ssw/sswConstr.c9
-rw-r--r--src/proof/ssw/sswCore.c2
-rw-r--r--src/proof/ssw/sswDyn.c9
-rw-r--r--src/proof/ssw/sswFilter.c9
-rw-r--r--src/proof/ssw/sswInt.h20
-rw-r--r--src/proof/ssw/sswIslands.c3
-rw-r--r--src/proof/ssw/sswLcorr.c6
-rw-r--r--src/proof/ssw/sswPairs.c12
-rw-r--r--src/proof/ssw/sswPart.c2
-rw-r--r--src/proof/ssw/sswRarity.c17
-rw-r--r--src/proof/ssw/sswRarity2.c14
-rw-r--r--src/proof/ssw/sswSat.c3
-rw-r--r--src/proof/ssw/sswSemi.c6
-rw-r--r--src/proof/ssw/sswSim.c8
-rw-r--r--src/proof/ssw/sswSimSat.c6
-rw-r--r--src/proof/ssw/sswSweep.c9
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 03:52:49 +0000