Silencing some of the gcc warnings.

12 files changed, 25 insertions, 25 deletions

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 );