Silencing some of the gcc warnings.

36 files changed, 45 insertions, 59 deletions

diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 287fd208..87eb5e6c 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -175,7 +175,7 @@ Vec_Ptr_t * Gia_VtaAbsToFrames( Vec_Int_t * vAbs )
 {
     Vec_Ptr_t * vFrames;
     Vec_Int_t * vFrame;
-    int i, k, Entry, iStart, iStop;
+    int i, k, Entry, iStart, iStop = -1;
     int nFrames = Vec_IntEntry( vAbs, 0 );
     assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
     vFrames = Vec_PtrAlloc( nFrames );
@@ -614,9 +614,6 @@ void Vta_ManSatVerify( Vta_Man_t * p )
         Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
         if ( Gia_ObjIsAnd(pObj) )
         {
-            int iVar  = Vta_ObjId(p, pThis);
-            int iVar0 = Vta_ObjId(p, pThis0);
-            int iVar1 = Vta_ObjId(p, pThis1);
             if ( pThis->Value == VTA_VAR1 )
                 assert( Vta_ValIs1(pThis0, Gia_ObjFaninC0(pObj)) && Vta_ValIs1(pThis1, Gia_ObjFaninC1(pObj)) );
             else if ( pThis->Value == VTA_VAR0 )
@@ -625,8 +622,6 @@ void Vta_ManSatVerify( Vta_Man_t * p )
         }
         else if ( Gia_ObjIsRo(p->pGia, pObj) )
         {
-            int VarA = Vta_ObjId(p,pThis);
-            int VarB = !pThis0 ? 0 : Vta_ObjId(p,pThis0);
             pObj = Gia_ObjRoToRi( p->pGia, pObj );
             if ( pThis->iFrame == 0 )
                 assert( pThis->Value == VTA_VAR0 );
@@ -966,7 +961,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pCex = Vga_ManDeriveCex( p );
     else
     {
-        int nObjOld = p->nObjs;
+//        int nObjOld = p->nObjs;
         Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
             if ( !Gia_ObjIsPi(p->pGia, pObj) )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );
@@ -1153,7 +1148,7 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
 void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames, int nConfls, int nCexes, int Time )
 {
     unsigned * pInfo;
-    int * pCountAll, * pCountUni;
+    int * pCountAll = NULL, * pCountUni = NULL;
     int i, k, iFrame, iObj, Entry;
     // print info about frames
     if ( vCore )
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 6da633e0..3c415707 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -570,7 +570,7 @@ int Gia_ManSolveSat( Gia_Man_t * p )
 {
 //    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
     Aig_Man_t * pNew;
-    int RetValue, clk = clock();
+    int RetValue;//, clk = clock();
     pNew = Gia_ManToAig( p, 0 );
     RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0, 0 );
     if ( RetValue == 0 )
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index abf378cb..5f1bb25d 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1450,13 +1450,13 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         assert( Vec_PtrSize(p->vNamesOut) == Gia_ManCoNum(p) );
         // write PIs
         Gia_ManForEachPi( p, pObj, i )
-            fprintf( pFile, "i%d %s\n", i, Vec_PtrEntry(p->vNamesIn, i) );
+            fprintf( pFile, "i%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, i) );
         // write latches
         Gia_ManForEachRo( p, pObj, i )
-            fprintf( pFile, "l%d %s\n", i, Vec_PtrEntry(p->vNamesIn, Gia_ManPiNum(p) + i) );
+            fprintf( pFile, "l%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesIn, Gia_ManPiNum(p) + i) );
         // write POs
         Gia_ManForEachPo( p, pObj, i )
-            fprintf( pFile, "o%d %s\n", i, Vec_PtrEntry(p->vNamesOut, i) );
+            fprintf( pFile, "o%d %s\n", i, (char *)Vec_PtrEntry(p->vNamesOut, i) );
     }
 
     // write the comment
diff --git a/src/aig/gia/giaBidec.c b/src/aig/gia/giaBidec.c
index 54f98afd..ae938798 100644
--- a/src/aig/gia/giaBidec.c
+++ b/src/aig/gia/giaBidec.c
@@ -241,7 +241,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
     Vec_Int_t * vLeaves, * vTruth, * vVisited;
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i, clk = clock();
+    int i;//, clk = clock();
     pPars->nVarsMax = Gia_ManLutSizeMax( p );
     pPars->fVerbose = fVerbose;
     if ( pPars->nVarsMax < 2 )
diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c
index b04d5953..6fbd1095 100644
--- a/src/aig/gia/giaCCof.c
+++ b/src/aig/gia/giaCCof.c
@@ -267,7 +267,7 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     Gia_Man_t * pNew;
     Ccf_Man_t * p;
     Gia_Obj_t * pObj;
-    int f, i, Lit, RetValue, fFailed = 0;
+    int f, i, Lit, RetValue = -1, fFailed = 0;
     int nTimeToStop = time(NULL) + nTimeMax;
     int clk = clock();
     assert( Gia_ManPoNum(pGia) == 1 );
diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c
index 7cfdac74..8cfa9efc 100644
--- a/src/aig/gia/giaCTas.c
+++ b/src/aig/gia/giaCTas.c
@@ -1245,7 +1245,7 @@ int Tas_ManPropagate( Tas_Man_t * p, int Level )
 {
     int hClause;
     Gia_Obj_t * pVar;
-    int i, k, nIter = 0;
+    int i, k;//, nIter = 0;
     while ( 1 )
     {
 //        nIter++;
@@ -1285,7 +1285,7 @@ int Tas_ManPropagate( Tas_Man_t * p, int Level )
 int Tas_ManSolve_rec( Tas_Man_t * p, int Level )
 { 
     Tas_Que_t * pQue = &(p->pClauses);
-    Gia_Obj_t * pVar, * pDecVar;
+    Gia_Obj_t * pVar, * pDecVar = NULL;
     int hClause, hLearn0, hLearn1;
     int iPropHead, iJustHead, iJustTail;
     // propagate assignments
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 69ae161f..342332cd 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -983,7 +983,7 @@ void Gia_ManPrintRepr( Gia_Man_t * p )
     int i;
     Gia_ManForEachObj( p, pObj, i )
         if ( ~p->pReprsOld[i] )
-            printf( "%d->%d ", i, p->pReprs[i] );
+            printf( "%d->%d ", i, p->pReprs[i].iRepr );
     printf( "\n" );
 }
 
@@ -1620,7 +1620,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
     Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pCopy;
-    int i, nFlops = 0;
+    int i;//, nFlops = 0;
     assert( Gia_ManPoNum(p) == 1 );
     assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
 
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 43724871..e244ef46 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1913,7 +1913,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
 {
     Vec_Int_t * vNodes;
     Gia_Man_t * pGia1, * pGia2, * pMiter;
-    Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj;
+    Gia_Obj_t * pObj1, * pObj2, * pObjM, * pObj = NULL;
     int i, k, iObj, iNext, iPrev, iRepr;
     int iLitsOld, iLitsNew;
     if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index e7abb555..94ad069b 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -714,7 +714,7 @@ Vec_Int_t * Frc_ManCollectCos( Frc_Man_t * p )
 void Frc_ManCrossCutTest( Frc_Man_t * p, Vec_Int_t * vOrderInit )
 {
     Vec_Int_t * vOrder;
-    int clk = clock();
+//    int clk = clock();
     vOrder = vOrderInit? vOrderInit : Frc_ManCollectCos( p );
     printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 0 ) );
     printf( "CrossCut = %6d\n", Frc_ManCrossCut( p, vOrder, 1 ) );
@@ -1072,7 +1072,7 @@ void For_ManFileExperiment()
     int RetValue;
 
     Size = (1 << Exp);
-    printf( "2^%d machine words (%d bytes).\n", Exp, sizeof(int) * Size );
+    printf( "2^%d machine words (%d bytes).\n", Exp, (int)sizeof(int) * Size );
 
     pBuffer = ABC_ALLOC( int, Size );
     for ( i = 0; i < Size; i++ )
diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
index 903a66e7..1d543a81 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -110,7 +110,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
     char * pFront;    // places used for the frontier
     int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
     int nCrossCutMaxInit = Gia_ManCrossCut( p );
-    int iFront = 0, clk = clock(); 
+    int iFront = 0;//, clk = clock(); 
     // set references for all objects
     Gia_ManSetRefs( p );
     // start the new manager
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index 35d076e5..0dfee293 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -506,7 +506,7 @@ void Gli_ManSwitching( Gli_Man_t * p )
 ***********************************************************************/
 void Gli_ManGlitching( Gli_Man_t * p )
 {
-    Gli_Obj_t * pThis, * pFanout, * pOther = Gli_ManObj(p, 41);
+    Gli_Obj_t * pThis, * pFanout;//, * pOther = Gli_ManObj(p, 41);
     int i, k, Handle;
 //    Gli_ManForEachObj( p, pThis, i )
 //        assert( pThis->fMark == 0 );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index e03439d0..2d8799da 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -98,7 +98,7 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
     If_Man_t * pIfMan;
     If_Obj_t * pIfObj;
     Gia_Obj_t * pNode;
-    int i, clk = clock();
+    int i;//, clk = clock();
     Gia_ManLevelNum( p );
 //    assert( p->pReprs == NULL );
 /*
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index c0feb735..8359146c 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -986,7 +986,7 @@ void Gia_IsoTest( Gia_Man_t * pGia )
 ***********************************************************************/
 Gia_Man_t * Gia_IsoFilterPos( Gia_Man_t * pGia, int fVerbose )
 {
-    int fVeryVerbose = 0;
+//    int fVeryVerbose = 0;
     Gia_IsoMan_t * p;
     Gia_Man_t * pTemp;
     Vec_Ptr_t * vBuffers, * vClasses;
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index c5ded61b..80fcf896 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -260,7 +260,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
 {
     Vec_Int_t * vSeens;  // objects seen so far
     Vec_Int_t * vAbs = p->vObjClasses;
-    int i, k, Entry, iStart, iStop, nFrames;
+    int i, k, Entry, iStart, iStop = -1, nFrames;
     int nObjBits, nObjMask, iObj, iFrame, nWords;
     unsigned * pInfo;
     int * pCountAll, * pCountUni;
diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c
index 07119daf..ad03f1e4 100644
--- a/src/aig/gia/giaShrink.c
+++ b/src/aig/gia/giaShrink.c
@@ -53,7 +53,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
     Gia_Obj_t * pObj, * pFanin;
     unsigned * pTruth;
     int i, k, iFan, clk = clock();
-    int ClassCounts[222] = {0};
+//    int ClassCounts[222] = {0};
     int * pLutClass, Counter = 0;
     assert( p->pMapping != NULL );
     if ( Gia_ManLutSizeMax( p ) > 4 )
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 180827b8..26adb84c 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2076,7 +2076,7 @@ void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
 {
     int i;
     for ( i = 0; i < p->nSatVars; i++ )
-        printf( "%d %.3f  ", i, (double)p->pSat->activity[i] );
+        printf( "%d %d  ", i, p->pSat->activity[i] );
     printf( "\n" );
 }
 
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index a5ec7dac..b2e61e61 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -246,7 +246,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
     int nUseStart = 0;
     Aig_Man_t * pAbs, * pTemp;
     Vec_Int_t * vFlops;
-    int Iter, clk = clock(), clk2 = clock();//, iFlop;
+    int Iter;//, clk = clock(), clk2 = clock();//, iFlop;
     assert( Aig_ManRegNum(p) > 0 );
     if ( pPars->fVerbose )
         printf( "Performing counter-example-based refinement.\n" );
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index 2e8e9cdc..4b219cac 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -322,7 +322,6 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
     nPrioOffset = pCex->nRegs;
     Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
     vRoots = Vec_IntAlloc( 1000 );
-//printf( "Const1 = %d  Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); 
     for ( f = 0; f <= pCex->iFrame; f++ )
     {
         int nPiCount = 0;
@@ -338,14 +337,8 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
             else if ( f == 0 )
                 Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
             else
-            {
-                Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
-                int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
                 Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
-            }
-//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
         }
-//printf( "\n" );
         // compute the PP info
         Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
     }
diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c
index 91bdf46f..fe7363b0 100644
--- a/src/aig/saig/saigConstr.c
+++ b/src/aig/saig/saigConstr.c
@@ -273,7 +273,7 @@ Vec_Ptr_t * Saig_ManDetectConstrCheckCont( Vec_Ptr_t * vSuper, Vec_Ptr_t * vSupe
 ***********************************************************************/
 int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
 {
-    Vec_Ptr_t * vSuper, * vSuper2, * vUnique;
+    Vec_Ptr_t * vSuper, * vSuper2 = NULL, * vUnique;
     Aig_Obj_t * pObj, * pObj2, * pFlop;
     int i, nFlops, RetValue;
     *pvOuts = NULL;
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index e60d1b82..cb43c5a2 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -202,7 +202,7 @@ int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerb
         Saig_ManForEachPo( p, pObj, i )
         {
             if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
-                printf( "Primary output :  ", i );
+                printf( "Primary output :  " );
             else
                 printf( "Constraint %3d :  ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p))  );
             printf( "ProbOne = %f  ",  (float)Vec_IntEntry(vProbs,  i)/(32*nWords*nFrames) );
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index d6af6e47..d1efca0b 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -246,7 +246,7 @@ Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p )
 { 
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
-    int i, nFlops = 0, RetValue;
+    int i, RetValue;
     assert( Saig_ManPoNum(p->pAig) == 1 );
     // start the new manager
     pNew = Aig_ManStart( 5000 );
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index c22cf415..cdc91759 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -451,7 +451,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     }
     if ( fVerbose )
     {
-        printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
+        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
index 4fa0012d..8417cbf5 100644
--- a/src/aig/saig/saigGlaPba2.c
+++ b/src/aig/saig/saigGlaPba2.c
@@ -412,7 +412,7 @@ Vec_Int_t * Aig_Gla3ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose
     }
     if ( fVerbose )
     {
-        printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
+        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index c9043ba2..33146077 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -150,7 +150,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
     Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
     Vec_Ptr_t * vTop, * vBot;
     Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
-    int i, k, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
+    int i, k, f, clk, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
     int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
     assert( fUnique == 0 || fUniqueAll == 0 );
     assert( Saig_ManPoNum(p) == 1 );
@@ -287,7 +287,7 @@ nextrun:
         {
             printf( "%4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ",
                 f, Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart), 
-                nSatVarNum, nClauses, pSat->stats.conflicts-nConfPrev );
+                nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev );
             ABC_PRT( "Time", clock() - clk );
         }
         if ( status == l_Undef )
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index ad6a9496..0e7c9de1 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -421,7 +421,7 @@ int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
 ***********************************************************************/
 Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
 {
-    int fVeryVerbose = 0;
+//    int fVeryVerbose = 0;
     Aig_Man_t * pPart, * pTemp;
     Vec_Ptr_t * vBuffers, * vClasses;
     Vec_Int_t * vLevel, * vRemain;
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
index 6556b90f..a415dcc8 100644
--- a/src/aig/saig/saigIsoFast.c
+++ b/src/aig/saig/saigIsoFast.c
@@ -181,7 +181,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
     Aig_Man_t * pAig = p->pAig;
     Aig_Obj_t * pObj;
     int i, Value, Entry, * pPerm;
-    int clk = clock();
+//    int clk = clock();
 
     assert( Aig_ObjIsPo(pPo) );
 
diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c
index 9279931f..6ec74112 100644
--- a/src/aig/saig/saigIsoSlow.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -318,7 +318,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
     Iso_Man_t * p;
     Iso_Obj_t * pIso;
     Aig_Obj_t * pObj;
-    int i, nNodes = 0, nEdges = 0;
+    int i;//, nNodes = 0, nEdges = 0;
     p = Iso_ManStart( pAig );
     Aig_ManForEachObj( pAig, pObj, i )
     {
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 20dbeec7..7fde61b1 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -608,8 +608,8 @@ int Saig_ManDemiterCheckPo( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t ** ppPo0,
     // make sure they can reach only one
     pObjR0 = Aig_Regular(pObj0);
     pObjR1 = Aig_Regular(pObj1);
-    if ( pObjR0->fMarkA && pObjR0->fMarkB || pObjR1->fMarkA && pObjR1->fMarkB || 
-         pObjR0->fMarkA && pObjR1->fMarkA || pObjR0->fMarkB && pObjR1->fMarkB )
+    if ( (pObjR0->fMarkA && pObjR0->fMarkB) || (pObjR1->fMarkA && pObjR1->fMarkB) || 
+         (pObjR0->fMarkA && pObjR1->fMarkA) || (pObjR0->fMarkB && pObjR1->fMarkB) )
          return 0;
 
     if ( pObjR1->fMarkA && !pObjR0->fMarkA )
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 4107c5a2..637da63e 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -259,7 +259,7 @@ Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref )
 {
     Vec_Int_t * vCounters;
     unsigned * pState;
-    int ValueThis, ValuePrev = -1, StepPrev = -1;
+    int ValueThis = -1, ValuePrev = -1, StepPrev = -1;
     int i, k, nRegs = p->pAig->nRegs;
     vCounters = Vec_IntStart( nPref );
     for ( i = 0; i < nRegs; i++ )
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index 632ad354..dcd95d36 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -508,7 +508,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
     Aig_Obj_t * pObj;
     Vec_Vec_t * vLits = NULL;
     Vec_Int_t * vAssumps, * vVar2PiId;
-    int i, k, f = 0, Entry, RetValue, Counter = 0;
+    int i, k, Entry, RetValue;//, f = 0, Counter = 0;
     int nCoreLits, * pCoreLits;
     int clk = clock();
     // create CNF
@@ -551,8 +551,6 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
     vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) );
     Aig_ManForEachPi( p->pFrames, pObj, i )
     {
-        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
-        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
 //        RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
 //        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
         Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index 021481b9..1b48d58b 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -149,7 +149,7 @@ int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo,
     int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 )
 {
     Aig_Obj_t * pFanout, * pObj = Aig_ManPi(p, iPi);
-    int i, k, f, iFanout, Value, Value2, Entry;
+    int i, k, f, iFanout = -1, Value, Value2, Entry;
     // save original value
     Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
     assert( Value == SAIG_ZER || Value == SAIG_ONE );
diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c
index 858c2b3b..fbd06ac7 100644
--- a/src/aig/saig/saigSimExt2.c
+++ b/src/aig/saig/saigSimExt2.c
@@ -173,7 +173,7 @@ int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo
 void Saig_ManSetAndDriveImplications_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Vec_Ptr_t * vSimInfo )
 {
     Aig_Obj_t * pFanout;
-    int k, iFanout, Value0, Value1;
+    int k, iFanout = -1, Value0, Value1;
     int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f );
     assert( !Saig_ManSimInfo2IsOld( Value ) );
     Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) );
diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c
index b8eed19e..e8e47a66 100644
--- a/src/aig/saig/saigSimFast.c
+++ b/src/aig/saig/saigSimFast.c
@@ -348,7 +348,7 @@ Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref,
     Vec_Int_t * vSwitching;
     int * pProbs;
     float * pSwitching;
-    int nFramesReal, clk, clkTotal = clock();
+    int nFramesReal, clk;//, clkTotal = clock();
     if ( fProbOne )
         fTrans = 0;
     vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 6579c37b..f22dfdc8 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -572,7 +572,7 @@ void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
 {
     Saig_MvObj_t * pEntry;
     unsigned * pState;
-    int i, k, j, nTotal = 0, Counter = 0, iFlop;
+    int i, k, j, nTotal = 0, iFlop;
     Vec_Int_t * vUniques = Vec_IntAlloc( 100 );
     Vec_Int_t * vCounter = Vec_IntAlloc( 100 );
     // count registers that never became undef
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
index cdf177d0..06890c7a 100644
--- a/src/aig/saig/saigStrSim.c
+++ b/src/aig/saig/saigStrSim.c
@@ -719,7 +719,7 @@ void Saig_StrSimSetContiguousMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
 void Ssw_StrSimMatchingExtendOne( 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/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c
index 01411c05..832d674b 100644
--- a/src/aig/saig/saigSwitch.c
+++ b/src/aig/saig/saigSwitch.c
@@ -268,7 +268,7 @@ Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref,
     Saig_SimObj_t * pAig, * pEntry;
     Vec_Int_t * vSwitching;
     float * pSwitching;
-    int nFramesReal, clk, clkTotal = clock();
+    int nFramesReal, clk;//, clkTotal = clock();
     vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
     pSwitching = (float *)vSwitching->pArray;
 clk = clock();
@@ -557,7 +557,7 @@ Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p )
         Aig_CManAddPo( pCMan, 
             (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj) ); 
     printf( "\nBytes alloc = %5d.  Bytes used = %7d.  Ave per node = %4.2f. \n", 
-        pCMan->nBytes, pCMan->pCur - pCMan->Data, 
+        pCMan->nBytes, (int)(pCMan->pCur - pCMan->Data), 
         1.0 * (pCMan->pCur - pCMan->Data) / (pCMan->nNodes + pCMan->nOuts ) );
 //    Aig_CManStop( pCMan );
     return pCMan;