Silencing some of the gcc warnings.

11 files changed, 19 insertions, 18 deletions

diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index fef0768a..b7d91dd9 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -615,7 +615,7 @@ cuddSwapping(
     int iterate;
     int previousSize;
     Move *moves, *move;
-    int pivot;
+    int pivot = -1;
     int modulo;
     int result;
 
diff --git a/src/map/if/ifDec10.c b/src/map/if/ifDec10.c
index 85c8625d..917f9f53 100644
--- a/src/map/if/ifDec10.c
+++ b/src/map/if/ifDec10.c
@@ -480,7 +480,7 @@ printf( "\n" );
 int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
 {
     int nSupp, fDerive = 0;
-    word z[2] = {0}, pF[16];
+    word pF[16];
     if ( nLeaves <= 6 )
         return 1;
     If_Dec10Copy( pF, (word *)pTruth, nVars );
diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c
index e624f889..442e1fa1 100644
--- a/src/map/if/ifDec16.c
+++ b/src/map/if/ifDec16.c
@@ -2012,10 +2012,10 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
     assert( G3.nVars == 0 );
     for ( i = 0; i < nLeaves; i++ )
         if ( !fUsed[i] )
-            G3.pVars[G3.nVars++] = i;
-    G3.pVars[G3.nVars++] = nLeaves;
+            G3.pVars[(int)G3.nVars++] = i;
+    G3.pVars[(int)G3.nVars++] = nLeaves;
     if ( G2.nVars )
-        G3.pVars[G3.nVars++] = nLeaves+1;
+        G3.pVars[(int)G3.nVars++] = nLeaves+1;
     assert( G1.nVars + G2.nVars + G3.nVars == nLeaves + 
         (G1.nVars > 0) + (G2.nVars > 0) + (G1.nMyu > 2) + (G2.nMyu > 2) );
     // what if both non-disjoint vars are the same???
@@ -2038,7 +2038,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
 ***********************************************************************/
 int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
 {
-    If_Grp_t G1 = {0}, G2 = {0}, G3 = {0};
+    If_Grp_t G1 = {0}, G3 = {0};
     int i, nLutLeaf, nLutLeaf2, nLutRoot, Length;
     // quit if parameters are wrong
     Length = strlen(pStr);
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 542ff258..2244fa26 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -37,7 +37,7 @@ static int           Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate );
 static unsigned      Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
 
 // fanout limits
-extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
+static const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/map/mio/exp.h b/src/map/mio/exp.h
index 40dff2e8..a76f33cb 100644
--- a/src/map/mio/exp.h
+++ b/src/map/mio/exp.h
@@ -153,7 +153,7 @@ static inline Vec_Int_t * Exp_Or( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int
 }
 static inline Vec_Int_t * Exp_Xor( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
 {
-    int i, v = 0, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
+    int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
     Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 5 );
     assert( (Len0 & 1) && (Len1 & 1) );
     Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 2)     );
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index f7eddab2..a4596c9f 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -41,7 +41,7 @@ static int Mio_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int Mio_CommandReadLibrary2( Abc_Frame_t * pAbc, int argc, char **argv );
 static int Mio_CommandPrintLibrary2( Abc_Frame_t * pAbc, int argc, char **argv );
-
+/*
 // internal version of GENLIB library
 static char * pMcncGenlib[25] = {
     "GATE inv1    1   O=!a;             PIN * INV     1 999 0.9 0.0 0.9 0.0\n",
@@ -66,7 +66,7 @@ static char * pMcncGenlib[25] = {
     "GATE zero    0   O=CONST0;\n",
     "GATE one     0   O=CONST1;\n"
 };
-
+*/
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecIso.c b/src/proof/cec/cecIso.c
index f1ca2ff7..990be5d1 100644
--- a/src/proof/cec/cecIso.c
+++ b/src/proof/cec/cecIso.c
@@ -170,7 +170,7 @@ static inline int Gia_ManIsoHashKey( int Id, unsigned * pStore, int nWords, int
 static inline void Gia_ManIsoTableAdd( Gia_Man_t * p, int Id, unsigned * pStore, int nWords, int * pTable, int nTableSize )
 {
     Gia_Obj_t * pTemp;
-    int Key, Ent, Counter = 0, Color = Gia_ObjColors( p, Id );
+    int Key, Ent, Color = Gia_ObjColors( p, Id );
     assert( Color == 1 || Color == 2 );
     Key = Gia_ManIsoHashKey( Id, pStore, nWords, nTableSize );
     for ( Ent = pTable[Key],  pTemp = (Ent ?  Gia_ManObj(p, Ent) : NULL);  pTemp;
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index 21ed8656..2ccbe524 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -185,7 +185,7 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
 {
     Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
     Cec_ManSim_t * pSim;
-    int RetValue, clkTotal = clock();
+    int RetValue;//, clkTotal = clock();
     assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
diff --git a/src/proof/fraig/fraigMan.c b/src/proof/fraig/fraigMan.c
index 0e1dcc66..125a4da1 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: %ld\n", (int)pParams->nTotalBacktrackLimit );
-    printf( "Total inspection limit: %ld\n", (int)pParams->nTotalInspectLimit );
+    printf( "Total conflict limit: %d\n", (int)pParams->nTotalBacktrackLimit );
+    printf( "Total inspection limit: %d\n", (int)pParams->nTotalInspectLimit );
     printf( "Parameter dump complete.\n" );
 }
 
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index a02ecc3f..80268a73 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -331,8 +331,8 @@ static inline void act_var_rescale(sat_solver2* s) {
     s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
 }
 static inline void act_clause_rescale(sat_solver2* s) {
-    static int Total = 0;
-    int i, clk = clock();
+//    static int Total = 0;
+    int i;//, clk = clock();
     unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
     for (i = 1; i < veci_size(&s->claActs); i++)
         claActs[i] >>= 14;
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 61c4d4d3..4bdefc6d 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -282,10 +282,11 @@ timeSelect += clock() - clk;
 int Msat_HeapCheck_rec( Msat_Order_t * p, int i )
 {
     return i >= HSIZE(p) ||
-        ( HPARENT(i) == 0 || 
         (
-           !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
+            ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
+
             Msat_HeapCheck_rec( p, HLEFT(i) ) && 
+            
             Msat_HeapCheck_rec( p, HRIGHT(i) )
         );
 }