Silencing some of the gcc warnings.

22 files changed, 37 insertions, 38 deletions

diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 6f3ce785..618d43d4 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -459,7 +459,7 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
     Vec_Ptr_t * vPres;
     int nWords = Vec_PtrReadWordsSimInfo(vInfo);
     int nBits = 32 * nWords; 
-    int k, nSize, iBit = 1, kMax = 0;
+    int k, nSize, kMax = 0;//, iBit = 1;
     vPat  = Vec_IntAlloc( 100 );
     vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
     Vec_PtrCleanSimInfo( vPres, 0, nWords );
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index b18a8fcd..238e3096 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -538,7 +538,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Fra_Man_t * pTemp;
     Aig_Man_t * pAigPart, * pAigTemp, * pAigNew = NULL;
     Vec_Int_t * vPart;
-    int i, nIter, timeSim, clk = clock(), clk2, clk3;
+    int i, nIter, timeSim, clk2, clk3, clk = clock();
     int TimeToStop = (TimeLimit == 0.0)? 0 : clock() + (int)(TimeLimit * CLOCKS_PER_SEC);
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
@@ -615,7 +615,6 @@ p->timePart += clock() - clk2;
         Vec_PtrClear( p->vFraigs );
         Vec_PtrForEachEntry( Vec_Int_t *, p->vParts, vPart, i )
         {
-            int clk3 = clock();
             if ( TimeLimit != 0.0 && clock() > TimeToStop )
             {
                 Vec_PtrForEachEntry( Aig_Man_t *, p->vFraigs, pAigPart, i )
diff --git a/src/proof/fraig/fraigMan.c b/src/proof/fraig/fraigMan.c
index ba08d793..0e1dcc66 100644
--- a/src/proof/fraig/fraigMan.c
+++ b/src/proof/fraig/fraigMan.c
@@ -103,8 +103,8 @@ void Prove_ParamsPrint( Prove_Params_t * pParams )
     printf( "BDD size limit for bailing out: %d\n", pParams->nBddSizeLimit );
     printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
     printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
-    printf( "Total conflict limit: %lld\n", pParams->nTotalBacktrackLimit );
-    printf( "Total inspection limit: %lld\n", pParams->nTotalInspectLimit );
+    printf( "Total conflict limit: %ld\n", (int)pParams->nTotalBacktrackLimit );
+    printf( "Total inspection limit: %ld\n", (int)pParams->nTotalInspectLimit );
     printf( "Parameter dump complete.\n" );
 }
 
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index 8af82f18..aed04632 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -80,7 +80,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     Inter_Man_t * p;
     Inter_Check_t * pCheck = NULL;
     Aig_Man_t * pAigTemp;
-    int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
+    int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp = 0;
     int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
 
     // sanity checks
diff --git a/src/proof/llb/llb1Pivot.c b/src/proof/llb/llb1Pivot.c
index d42bf659..688060bc 100644
--- a/src/proof/llb/llb1Pivot.c
+++ b/src/proof/llb/llb1Pivot.c
@@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
 int Llb_ManTracePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pPivot )
 {
     Aig_Obj_t * pFanout;
-    int k, iFan;
+    int k, iFan = -1;
     if ( Aig_ObjIsTravIdPrevious(p, pObj) )
         return 0;
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c
index fbf91351..722a8342 100644
--- a/src/proof/llb/llb1Reach.c
+++ b/src/proof/llb/llb1Reach.c
@@ -465,7 +465,7 @@ Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p )
 {
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
-    DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing;
+    DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
     int i, v, RetValue, nPiOffset;
     char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
     assert( Vec_PtrSize(p->vRings) > 0 );
@@ -582,7 +582,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
     DdNode * bConstrCs, * bConstrNs;
     int clk2, clk = clock(), nIters, nBddSize = 0;
-    int nThreshold = 10000;
+//    int nThreshold = 10000;
 
     // compute time to stop
     p->pPars->TimeTarget = p->pPars->TimeLimit ? time(NULL) + p->pPars->TimeLimit : 0;
diff --git a/src/proof/llb/llb1Sched.c b/src/proof/llb/llb1Sched.c
index 6bdae42e..51de973a 100644
--- a/src/proof/llb/llb1Sched.c
+++ b/src/proof/llb/llb1Sched.c
@@ -80,7 +80,7 @@ void Llb_MtrSwapColumns( Llb_Mtr_t * p, int iCol1, int iCol2 )
 int Llb_MtrFindBestColumn( Llb_Mtr_t * p, int iGrpStart )
 {
     int Cost, Cost2, CostBest = ABC_INFINITY, Cost2Best = ABC_INFINITY;
-    int WeightCur, WeightBest = -ABC_INFINITY, iGrp, iGrpBest = -1;
+    int WeightCur, WeightBest = -ABC_INFINITY, iGrp = -1, iGrpBest = -1;
     int k, c, iVar, Counter;
     // find partition that reduces partial product as much as possible
     for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ )
diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c
index c15574c2..626acbd2 100644
--- a/src/proof/llb/llb2Core.c
+++ b/src/proof/llb/llb2Core.c
@@ -99,7 +99,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
-    DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing;
+    DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
     int i, v, RetValue, nPiOffset;
     char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
     assert( Vec_PtrSize(p->vRings) > 0 );
@@ -209,7 +209,7 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ
     int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo );
     int * pGlo2Loc  = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
     DdNode * bCurrent, * bReached, * bNext, * bTemp;
-    int clk2, clk = clock(), nIters, nBddSize, iOutFail = -1;
+    int clk2, clk = clock(), nIters, nBddSize;//, iOutFail = -1;
 /*
     // compute time to stop
     if ( p->pPars->TimeLimit )
@@ -533,7 +533,7 @@ Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t
 {
     DdManager * dd;
     Vec_Ptr_t * vDdMans;
-    Vec_Ptr_t * vLower, * vUpper;
+    Vec_Ptr_t * vLower, * vUpper = NULL;
     int i;
     vDdMans = Vec_PtrStart( Vec_PtrSize(vResult) );
     Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i )
diff --git a/src/proof/llb/llb2Driver.c b/src/proof/llb/llb2Driver.c
index 041a39d5..4998b1ad 100644
--- a/src/proof/llb/llb2Driver.c
+++ b/src/proof/llb/llb2Driver.c
@@ -161,7 +161,7 @@ DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager
 ***********************************************************************/
 DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int TimeTarget )
 {
-    int fVerbose = 1;
+//    int fVerbose = 1;
     DdManager * dd;
     DdNode * bVar1, * bVar2, * bProd, * bRes, * bTemp;
     Aig_Obj_t * pObj;
diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c
index ebb4e038..544d7c04 100644
--- a/src/proof/llb/llb2Flow.c
+++ b/src/proof/llb/llb2Flow.c
@@ -273,7 +273,7 @@ int Llb_ManCutLiNum( Aig_Man_t * p, Vec_Ptr_t * vMinCut )
 {
     Aig_Obj_t * pFanout;
     Aig_Obj_t * pObj;
-    int i, k, iFanout, Counter = 0;
+    int i, k, iFanout = -1, Counter = 0;
     Vec_PtrForEachEntry( Aig_Obj_t *, vMinCut, pObj, i )
     {
         if ( Aig_ObjIsPi(pObj) )
@@ -1018,7 +1018,7 @@ void Llb_ManFlowUnmarkCone( Aig_Man_t * p, Vec_Ptr_t * vCone )
 void Llb_ManFlowCollectAndMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vCone )
 {
     Aig_Obj_t * pFanout;
-    int i, iFanout;
+    int i, iFanout = -1;
     if ( Saig_ObjIsLi(p, pObj) )
         return;
     if ( pObj->fMarkB )
@@ -1225,7 +1225,7 @@ Vec_Ptr_t * Llb_ManFlowFindBestCut( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t
 Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryVerbose )
 {
     int nVolMax = Aig_ManNodeNum(p) / Num;
-    Vec_Ptr_t * vResult, * vMinCut, * vLower, * vUpper;
+    Vec_Ptr_t * vResult, * vMinCut = NULL, * vLower, * vUpper;
     int i, k, nVol, clk = clock();
     vResult = Vec_PtrAlloc( 100 );
     Vec_PtrPush( vResult, Llb_ManComputeCutLo(p) );
@@ -1336,7 +1336,7 @@ void Llb_ManMinCutTest( Aig_Man_t * pAig, int Num )
     extern void Llb_BddExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, Vec_Ptr_t * vMaps );
  
 
-    int fVerbose = 1;
+//    int fVerbose = 1;
     Gia_ParLlb_t Pars, * pPars = &Pars;
     Vec_Ptr_t * vResult;//, * vSupps, * vMaps;
     Aig_Man_t * p;
diff --git a/src/proof/llb/llb2Image.c b/src/proof/llb/llb2Image.c
index 5baa5c57..99ffbdc4 100644
--- a/src/proof/llb/llb2Image.c
+++ b/src/proof/llb/llb2Image.c
@@ -121,7 +121,7 @@ Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vSt
 void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose )
 {
     Vec_Int_t * vOne;
-    int nVarsAll, Counter, iSupp, Entry, i, k;
+    int nVarsAll, Counter, iSupp = -1, Entry, i, k;
     // start quantification arrays
     *pvQuant0 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
     *pvQuant1 = Vec_PtrAlloc( Vec_PtrSize(vSupps) );
@@ -362,7 +362,7 @@ DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager *
     Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs, 
     int TimeTarget, int fBackward, int fReorder, int fVerbose )
 {
-    int fCheckSupport = 0;
+//    int fCheckSupport = 0;
     DdManager * ddPart;
     DdNode * bImage, * bGroup, * bCube, * bTemp;
     int i, clk, clk0 = clock();
diff --git a/src/proof/llb/llb3Image.c b/src/proof/llb/llb3Image.c
index f674d4b1..708af6d5 100644
--- a/src/proof/llb/llb3Image.c
+++ b/src/proof/llb/llb3Image.c
@@ -345,8 +345,8 @@ int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2,
     Vec_Ptr_t * vSingles;
     DdNode * bCube, * bFunc;
     int i, RetValue, nSuppSize;
-    int iPart1 = pPart1->iPart;
-    int iPart2 = pPart2->iPart;
+//    int iPart1 = pPart1->iPart;
+//    int iPart2 = pPart2->iPart;
 
     // create cube to be quantified
     bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c
index 45f6f11e..d28edecc 100644
--- a/src/proof/llb/llb3Nonlin.c
+++ b/src/proof/llb/llb3Nonlin.c
@@ -247,7 +247,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Vec_Int_t * vVarsNs;
-    DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing;
+    DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
     int i, v, RetValue, nPiOffset;
     char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
     assert( Vec_PtrSize(p->vRings) > 0 );
@@ -428,7 +428,7 @@ int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev )
 int Llb_NonlinReachability( Llb_Mnn_t * p )
 { 
     DdNode * bTemp, * bNext;
-    int nIters, nBddSize0, nBddSize, NumCmp, Limit = p->pPars->nBddMax;
+    int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax;
     int clk2, clk3, clk = clock();
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c
index a68be711..3a1c96e5 100644
--- a/src/proof/llb/llb4Cex.c
+++ b/src/proof/llb/llb4Cex.c
@@ -52,7 +52,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int
     sat_solver * pSat;
     Aig_Obj_t * pObj;
     unsigned * pNext, * pThis;
-    int i, k, iBit, status, nRegs, clk = clock();
+    int i, k, iBit, status, nRegs;//, clk = clock();
 /*
     Vec_PtrForEachEntry( unsigned *, vStates, pNext, i )
     {
diff --git a/src/proof/llb/llb4Image.c b/src/proof/llb/llb4Image.c
index 91eb62f8..039be164 100644
--- a/src/proof/llb/llb4Image.c
+++ b/src/proof/llb/llb4Image.c
@@ -323,8 +323,8 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2
     Vec_Ptr_t * vSingles;
     DdNode * bCube, * bFunc;
     int i, RetValue, nSuppSize;
-    int iPart1 = pPart1->iPart;
-    int iPart2 = pPart2->iPart;
+//    int iPart1 = pPart1->iPart;
+//    int iPart2 = pPart2->iPart;
     int liveBeg, liveEnd;
 
     // create cube to be quantified
@@ -806,7 +806,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV
     Vec_Ptr_t * vGroups;
     Llb_Prt_t * pPart, * pPart1, * pPart2;
     Llb_Mgr_t * p;
-    int i, nReorders, clk = clock();
+    int i, nReorders;//, clk = clock();
     // start the manager
     p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
     // remove singles
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
index b7ea79b8..6442d62e 100644
--- a/src/proof/llb/llb4Nonlin.c
+++ b/src/proof/llb/llb4Nonlin.c
@@ -576,8 +576,8 @@ Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose )
     Vec_Int_t * vVars2Q;
     Vec_Ptr_t * vStates, * vRootsNew;
     Aig_Obj_t * pObj;
-    DdNode * bState, * bImage, * bOneCube, * bRing;
-    int i, v, RetValue, clk = clock();
+    DdNode * bState = NULL, * bImage, * bOneCube, * bRing;
+    int i, v, RetValue;//, clk = clock();
     char * pValues;
     assert( Vec_PtrSize(p->vRings) > 0 );
     // disable the timeout
@@ -666,7 +666,7 @@ Vec_Ptr_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p, int fBackward, int fVerbose )
 int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
 { 
     DdNode * bAux;
-    int nIters, nBddSizeFr, nBddSizeTo, nBddSizeTo2;
+    int nIters, nBddSizeFr = 0, nBddSizeTo = 0, nBddSizeTo2 = 0;
     int clkTemp, clkIter, clk = clock();
     assert( Aig_ManRegNum(p->pAig) > 0 );
 
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 2524d380..02cb4876 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -549,7 +549,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     int fPrintClauses = 0;
     Pdr_Set_t * pCube;
     int k, RetValue = -1;
-    int clkTotal = clock();
+//    int clkTotal = clock();
     int clkStart = clock();
     p->timeToStop = p->pPars->nTimeOut ? time(NULL) + p->pPars->nTimeOut : 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 6fec1605..32843489 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -199,7 +199,7 @@ int Pdr_ManSimDataInit( Aig_Man_t * pAig,
 int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
 {
     Aig_Obj_t * pFanout;
-    int i, k, iFanout, Value, Value2;
+    int i, k, iFanout = -1, Value, Value2;
     assert( Saig_ObjIsLo(pAig, pObj) );
     assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
     // save original value
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index dd075f44..95f029d4 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -499,7 +499,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
 ***********************************************************************/
 int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )
 {
-    Aig_Man_t * pAig = p->pAig;
+//    Aig_Man_t * pAig = p->pAig;
     Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
     Aig_Obj_t * pObj, * pTemp, * pRepr;
     int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 380ac7e5..4f6fb26e 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -382,7 +382,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 r, TimeLimitPart;//, clkTotal = clock();
     int nTimeToStop = TimeLimit ? TimeLimit + time(NULL) : 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index 0802aca5..ca95cf23 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -130,7 +130,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
 void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
 {
     Aig_Obj_t * pNext, * pObj;
-    int i, k, iFan;
+    int i, k, iFan = -1;
     Vec_PtrClear( vNodes );
     Aig_ManIncrementTravId( p );
     Aig_ManForEachObj( p, pObj, i )
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 264bb2c8..25a80be7 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -895,7 +895,7 @@ 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, clk, clkTotal = clock();
+    int r, f = -1, clk, clkTotal = clock();
     int nTimeToStop = time(NULL) + TimeOut;
     int RetValue = -1;
     int iFrameFail = -1;
@@ -1012,7 +1012,7 @@ 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, i, k, clkTotal = clock();
+    int r, f = -1, i, k, clkTotal = clock();
     int nTimeToStop = time(NULL) + TimeOut;
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );