Silencing some of the gcc warnings.

115 files changed, 234 insertions, 254 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;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e15b7402..16c9ffe7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25700,7 +25700,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_Man_t * pTemp = NULL;
+//    Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int fUseCubes = 1;
     int fMiter = 0;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index a3a12b71..6c2296b9 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -1485,12 +1485,12 @@ void Abc_NtkShow6VarFunc( char * pF0, char * pF1 )
     word F0, F1;
     if ( strlen(pF0) != 16 )
     {
-        printf( "Wrong length (%d) of 6-var truth table.\n", strlen(pF0) );
+        printf( "Wrong length (%d) of 6-var truth table.\n", (int)strlen(pF0) );
         return;
     }
     if ( strlen(pF1) != 16 )
     {
-        printf( "Wrong length (%d) of 6-var truth table.\n", strlen(pF1) );
+        printf( "Wrong length (%d) of 6-var truth table.\n", (int)strlen(pF1) );
         return;
     }
     Extra_ReadHexadecimal( (unsigned *)&F0, pF0, 6 );
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 93b17c37..303f9617 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -21,11 +21,17 @@
 
 // The code in this file is developed in collaboration with Mark Jarvin of Toronto.
 
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include <stdarg.h>
+
 #include "src/misc/bzlib/bzlib.h"
+#include "src/misc/zlib/zlib.h"
 #include "ioAbc.h"
 
-#include <stdarg.h>
-#include "src/misc/zlib/zlib.h"
 
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index d8d3f787..fe4266b0 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -388,8 +388,6 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     if ( pNtk->vRealNodes )
     {
         Abc_Obj_t * pObj;
-        int Num1 = Vec_IntSize(pNtk->vRealNodes);
-        int Num2 = Abc_NtkPoNum(pNtk)-pNtk->nRealPos;
         fprintf( pFile, "\n\n" );
         assert( Vec_IntSize(pNtk->vRealNodes) == Abc_NtkPoNum(pNtk)-pNtk->nRealPos );
         Abc_NtkForEachObjVec( pNtk->vRealNodes, pNtk, pObj, i )
@@ -723,7 +721,7 @@ void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCover )
         extern word If_Dec7Perform( word t[2], int fDerive );
 
         char * pSop;
-        word z, uTruth6, uTruth7[2], Cofs6[2], Cofs7[2][2];
+        word z, uTruth6 = 0, uTruth7[2], Cofs6[2], Cofs7[2][2];
         int c, iVar, nVarsMin[2], pVars[2][10];
 
         // collect variables
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 1a924c31..4c40346c 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -2051,10 +2051,6 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox )
     assert( Ver_NtkIsDefined(pNtkBox) );
     assert( !Abc_NtkHasBlackbox(pNtkBox) || Abc_NtkBoxNum(pNtkBox) == 1 );
 
-    if ( !strcmp(pNtkBox->pName,"add_4u_4u") )
-    {
-        int s = 0;
-    }
 /*
     // clean the PI/PO nets
     Abc_NtkForEachPi( pNtkBox, pTerm, i )
diff --git a/src/bdd/cudd/cuddAPI.c b/src/bdd/cudd/cuddAPI.c
index 6456d17c..800e01c1 100644
--- a/src/bdd/cudd/cuddAPI.c
+++ b/src/bdd/cudd/cuddAPI.c
@@ -3067,7 +3067,7 @@ Cudd_PrintInfo(
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Number of dead ZDD nodes: %u\n", dd->deadZ);
     if (retval == EOF) return(0);
-    retval = fprintf(fp,"Total number of nodes allocated: %d\n", dd->allocated);
+    retval = fprintf(fp,"Total number of nodes allocated: %d\n", (int)dd->allocated);
     if (retval == EOF) return(0);
     retval = fprintf(fp,"Total number of nodes reclaimed: %.0f\n",
                      dd->reclaimed);
diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c
index b9b8c3e3..29307756 100644
--- a/src/bdd/cudd/cuddAddIte.c
+++ b/src/bdd/cudd/cuddAddIte.c
@@ -451,7 +451,7 @@ cuddAddIteRecur(
     DdNode *one,*zero;
     DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
     unsigned int topf,topg,toph,v;
-    int index;
+    int index = -1;
 
     statLine(dd);
     /* Trivial cases. */
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index d3386088..18ebee20 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -639,7 +639,7 @@ cuddBddIteRecur(
     DdNode       *one, *zero, *res;
     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
     unsigned int topf, topg, toph, v;
-    int          index;
+    int          index = -1;
     int          comple;
 
     statLine(dd);
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 99aa9348..ff31e04c 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -1693,7 +1693,7 @@ BuildConjuncts(
   st_table * mintermTable)
 {
     int topid, distance;
-    Conjuncts *factorsNv, *factorsNnv, *factors;
+    Conjuncts *factorsNv = NULL, *factorsNnv = NULL, *factors;
     Conjuncts *dummy;
     DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
     double minNv = 0.0, minNnv = 0.0;
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c
index 598cc9a1..547810b2 100644
--- a/src/bdd/cudd/cuddGroup.c
+++ b/src/bdd/cudd/cuddGroup.c
@@ -456,7 +456,7 @@ ddReorderChildren(
   Cudd_ReorderingType method)
 {
     int lower;
-    int upper;
+    int upper = -1;
     int result;
     unsigned int initialSize;
 
@@ -1494,7 +1494,7 @@ ddGroupMove(
     Move *move;
     int  size;
     int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-    int  swapx,swapy;
+    int  swapx = -1,swapy = -1;
 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
     int  initialSize,bestSize;
 #endif
@@ -1674,7 +1674,7 @@ ddGroupSiftingBackward(
 {
     Move *move;
     int  res;
-    Move *end_move;
+    Move *end_move = NULL;
     int diff, tmp_diff;
     int index;
     unsigned int pairlev;
diff --git a/src/bdd/cudd/cuddHarwell.c b/src/bdd/cudd/cuddHarwell.c
index b61af2e0..02018a11 100644
--- a/src/bdd/cudd/cuddHarwell.c
+++ b/src/bdd/cudd/cuddHarwell.c
@@ -144,7 +144,7 @@ Cudd_addHarwell(
     DdNode *cubex, *cubey, *minterm1;
     int u, v, err, i, j, nv;
     double val;
-    DdNode **lx, **ly, **lxn, **lyn;    /* local copies of x, y, xn, yn_ */
+    DdNode **lx = NULL, **ly = NULL, **lxn = NULL, **lyn = NULL;    /* local copies of x, y, xn, yn_ */
     int lnx, lny;                       /* local copies of nx and ny */
     char title[73], key[9], mxtype[4], rhstyp[4];
     int totcrd, ptrcrd, indcrd, valcrd, rhscrd,
diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
index 601b6496..38f75beb 100644
--- a/src/bdd/cudd/cuddLinear.c
+++ b/src/bdd/cudd/cuddLinear.c
@@ -377,7 +377,7 @@ cuddLinearInPlace(
     int    posn;
     int    isolated;
     DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
-    DdNode *g,*next,*last;
+    DdNode *g,*next,*last=NULL;
     DdNodePtr *previousP;
     DdNode *tmp;
     DdNode *sentinel = &(table->sentinel);
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c
index 2ecc1636..ab362dea 100644
--- a/src/bdd/cudd/cuddPriority.c
+++ b/src/bdd/cudd/cuddPriority.c
@@ -790,7 +790,7 @@ Cudd_Inequality(
         int leftChild, middleChild, rightChild;
         DdNode *g0, *g1, *fplus, *fequal, *fminus;
         int j;
-        DdNode *newMap[2];
+        DdNode *newMap[2] = {NULL};
         int newIndex[2];
 
         kTrueLower = kTrue;
@@ -978,7 +978,7 @@ Cudd_Disequality(
         int leftChild, middleChild, rightChild;
         DdNode *g0, *g1, *fplus, *fequal, *fminus;
         int j;
-        DdNode *newMap[2];
+        DdNode *newMap[2] = {NULL};
         int newIndex[2];
 
         kTrueLbLower = kTrueLb;
@@ -1430,7 +1430,7 @@ cuddCProjectionRecur(
 {
     DdNode *res, *res1, *res2, *resA;
     DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
-    unsigned int topR, topY, top, index;
+    unsigned int topR, topY, top, index = 0;
     DdNode *one = DD_ONE(dd);
 
     statLine(dd);
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index 5eb3e099..b5673d88 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -1261,12 +1261,12 @@ BuildSubsetBdd(
 {
     DdNode *N, *Nv, *Nnv;
     DdNode *ThenBranch, *ElseBranch, *childBranch;
-    DdNode *child, *regChild, *regNnv, *regNv;
+    DdNode *child, *regChild, *regNnv = NULL, *regNv = NULL;
     NodeDist_t *nodeStatNv, *nodeStat, *nodeStatNnv;
     DdNode *neW, *topv, *regNew;
     char *entry;
     unsigned int topid;
-    unsigned int childPathLength, oddLen, evenLen, NnvPathLength, NvPathLength;
+    unsigned int childPathLength, oddLen, evenLen, NnvPathLength = 0, NvPathLength = 0;
     unsigned int NvBotDist, NnvBotDist;
     int tiebreakChild;
     int  processingDone, thenDone, elseDone;
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index 630c3778..dfdc6c85 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -1479,10 +1479,10 @@ ddSymmGroupMove(
   Move ** moves)
 {
     Move *move;
-    int  size;
+    int  size = -1;
     int  i,j;
     int  xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-    int  swapx,swapy;
+    int  swapx = -1,swapy = -1;
 
 #ifdef DD_DEBUG
     assert(x < y);      /* we assume that x < y */
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c
index f64f1f8e..a45a1efd 100644
--- a/src/bdd/cudd/cuddTable.c
+++ b/src/bdd/cudd/cuddTable.c
@@ -1804,7 +1804,7 @@ cuddInsertSubtables(
     int oldsize,newsize;
     int i,j,index,reorderSave;
     unsigned int numSlots = unique->initSlots;
-    int *newperm, *newinvperm, *newmap;
+    int *newperm, *newinvperm, *newmap=NULL;
     DdNode *one, *zero;
 
 #ifdef DD_DEBUG
diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c
index 046c1957..8a1f9b2c 100644
--- a/src/bdd/cudd/cuddUtil.c
+++ b/src/bdd/cudd/cuddUtil.c
@@ -1404,7 +1404,7 @@ Cudd_bddPickArbitraryMinterms(
     DdNode **old, *neW;
     double minterms;
     char *saveString;
-    int saveFlag, savePoint, isSame;
+    int saveFlag, savePoint = -1, isSame;
 
     minterms = Cudd_CountMinterm(dd,f,n);
     if ((double)k > minterms) {
diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c
index 2d2a5049..dfdf8bb3 100644
--- a/src/bdd/cudd/cuddZddGroup.c
+++ b/src/bdd/cudd/cuddZddGroup.c
@@ -436,7 +436,7 @@ zddReorderChildren(
   Cudd_ReorderingType method)
 {
     int lower;
-    int upper;
+    int upper = -1;
     int result;
     unsigned int initialSize;
 
@@ -1084,7 +1084,7 @@ zddGroupMove(
     Move *move;
     int  size;
     int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
-    int  swapx,swapy;
+    int  swapx=-1,swapy=-1;
 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
     int  initialSize,bestSize;
 #endif
diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c
index 8a7ae526..8a1d14cb 100644
--- a/src/bdd/cudd/cuddZddReord.c
+++ b/src/bdd/cudd/cuddZddReord.c
@@ -495,7 +495,7 @@ cuddZddSwapInPlace(
     int         i;
     int         posn;
     DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
-    DdNode      *newf1, *newf0, *next;
+    DdNode      *newf1=NULL, *newf0, *next;
     DdNodePtr   g, *lastP, *previousP;
 
 #ifdef DD_DEBUG
@@ -756,7 +756,7 @@ cuddZddSwapping(
     int iterate;
     int previousSize;
     Move *moves, *move;
-    int pivot;
+    int pivot = -1;
     int modulo;
     int result;
 
diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c
index 4979968a..f04772c9 100644
--- a/src/bdd/cudd/cuddZddSymm.c
+++ b/src/bdd/cudd/cuddZddSymm.c
@@ -1487,7 +1487,7 @@ zdd_group_move(
     Move        *move;
     int         size;
     int         i, temp, gxtop, gxbot, gybot, yprev;
-    int         swapx, swapy;
+    int         swapx = -1, swapy = -1;
 
 #ifdef DD_DEBUG
     assert(x < y);      /* we assume that x < y */
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 7fd64d75..df8b5cf0 100644
--- a/src/bdd/reo/reoTransfer.c
+++ b/src/bdd/reo/reoTransfer.c
@@ -72,7 +72,7 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     if ( cuddIsConstant(F) )
     {
         pUnit->lev    = REO_CONST_LEVEL;
-        pUnit->pE     = (reo_unit*)((int)(ABC_PTRUINT_T)(cuddV(F)));
+        pUnit->pE     = (reo_unit*)(ABC_PTRUINT_T)(cuddV(F));
         pUnit->pT     = NULL;
         // check if the diagram that is being reordering has complement edges
         if ( F != dd->one )
diff --git a/src/bool/bdc/bdcSpfd.c b/src/bool/bdc/bdcSpfd.c
index 3144f136..26eccac7 100644
--- a/src/bool/bdc/bdcSpfd.c
+++ b/src/bool/bdc/bdcSpfd.c
@@ -602,7 +602,7 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
     for ( q = p; q < p+nFuncs; q++ )
        q->iList = 0;
     q = p + 1;
-    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
+    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
 
     vTruths  = Vec_WrdStart( nFuncs );
     vWeights = Vec_IntStart( nFuncs );
@@ -624,7 +624,7 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
         Vec_IntPush( vWeights, 0 );
     }
     Vec_IntPush( vStops, 7 );
-    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, q-p );
+    printf( "Added %d + %d + 0 = %d. Total = %8d.\n", 0, 0, 0, (int)(q-p) );
 
     // create gates
     for ( n = 0; n < Limit; n++ )
@@ -643,7 +643,7 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
             pEnd1 = p + Vec_IntEntry( vStops, m+1 );
 
             clk2 = clock();
-            printf( "Trying %7d  x %7d.  ", pEnd0-pBeg0, pEnd1-pBeg1 );
+            printf( "Trying %7d  x %7d.  ", (int)(pEnd0-pBeg0), (int)(pEnd1-pBeg1) );
             for ( pThis0 = pBeg0; pThis0 < pEnd0; pThis0++ )
             for ( pThis1 = pBeg1; pThis1 < pEnd1; pThis1++ )
             if ( k < m || pThis1 > pThis0 )
@@ -679,7 +679,7 @@ Vec_Wrd_t * Bdc_SpfdDecomposeTest__( Vec_Int_t ** pvWeights )
                     goto finish;
                 }
             }
-            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", k, m, n+1, q-p );
+            printf( "Added %d + %d + 1 = %d. Total = %8d.   ", k, m, n+1, (int)(q-p) );
             Abc_PrintTime( 1, "Time", clock() - clk2 );
         }
         Vec_IntPush( vStops, q-p );
@@ -804,7 +804,7 @@ int Bdc_SpfdComputeCost( word f, int i, Vec_Int_t * vWeights )
 word Bdc_SpfdFindBest( Vec_Wrd_t * vDivs, Vec_Int_t * vWeights, word F0, word F1, int * pCost )
 {
     word Func, FuncBest;
-    int i, Cost, CostBest = -1, NumBest;
+    int i, Cost, CostBest = -1, NumBest = -1;
     Vec_WrdForEachEntry( vDivs, Func, i )
     {
         if ( (Func & F0) == 0 )
diff --git a/src/map/amap/amapLib.c b/src/map/amap/amapLib.c
index bbf76a64..b11e3222 100644
--- a/src/map/amap/amapLib.c
+++ b/src/map/amap/amapLib.c
@@ -261,7 +261,7 @@ Vec_Ptr_t * Amap_LibSelectGates( Amap_Lib_t * p, int fVerbose )
 {
     Vec_Ptr_t * vSelect;
     Amap_Gat_t * pGate, * pGate2;
-    int i, k, clk = clock();
+    int i, k;//, clk = clock();
     p->pGate0   = Amap_LibFindGate( p, 0 );
     p->pGate1   = Amap_LibFindGate( p, ~0 );
     p->pGateBuf = Amap_LibFindGate( p, 0xAAAAAAAA );
@@ -343,8 +343,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
     p->vSelect = Amap_LibSelectGates( p, fVerbose );
     if ( fVerbose )
     {
-        printf( "Selected %d functionally unique gates. ",
-            Vec_PtrSize(p->vSelect), Vec_PtrSize(p->vSorted) );
+        printf( "Selected %d functionally unique gates. ", Vec_PtrSize(p->vSelect) );
         ABC_PRT( "Time", clock() - clk );
 //       Amap_LibPrintSelectedGates( p, 0 );
     }
@@ -352,8 +351,7 @@ Amap_Lib_t * Amap_LibReadAndPrepare( char * pFileName, int fVerbose, int fVeryVe
     Amap_LibCreateRules( p, fVeryVerbose );
     if ( fVerbose )
     {
-        printf( "Created %d rules and %d matches. ", 
-            p->nNodes, p->nSets );
+        printf( "Created %d rules and %d matches. ", p->nNodes, p->nSets );
         ABC_PRT( "Time", clock() - clk );
     }
     return p;
diff --git a/src/map/amap/amapLiberty.c b/src/map/amap/amapLiberty.c
index c31bc141..49b36848 100644
--- a/src/map/amap/amapLiberty.c
+++ b/src/map/amap/amapLiberty.c
@@ -722,6 +722,7 @@ int Amap_LibertyBuildItem( Amap_Tree_t * p, char ** ppPos, char * pEnd )
     Amap_Item_t * pItem;
     Amap_Pair_t Key, Head, Body;
     char * pNext, * pStop;
+    Key.End = 0;
     if ( Amap_LibertySkipSpaces( p, ppPos, pEnd, 0 ) )
         return -2;
     Key.Beg = *ppPos - p->pContents;
diff --git a/src/map/amap/amapMatch.c b/src/map/amap/amapMatch.c
index 40409e0d..4c213f9c 100644
--- a/src/map/amap/amapMatch.c
+++ b/src/map/amap/amapMatch.c
@@ -433,7 +433,7 @@ static inline void Amap_ManMatchGetExacts( Amap_Man_t * p, Amap_Obj_t * pNode, A
 ***********************************************************************/
 void Amap_ManMatchNode( Amap_Man_t * p, Amap_Obj_t * pNode, int fFlow, int fRefs )
 {
-    Amap_Mat_t M1, M2, * pMBest = &M1, * pMThis = &M2;
+    Amap_Mat_t M1 = {0}, M2 = {0}, * pMBest = &M1, * pMThis = &M2;
     Amap_Cut_t * pCut;
     Amap_Set_t * pSet;
     Amap_Nod_t * pNod;
diff --git a/src/map/amap/amapMerge.c b/src/map/amap/amapMerge.c
index c52642e3..19470d63 100644
--- a/src/map/amap/amapMerge.c
+++ b/src/map/amap/amapMerge.c
@@ -520,7 +520,7 @@ void Amap_ManMerge( Amap_Man_t * p )
         Amap_ManMergeNodeCuts( p, pObj );
     if ( p->pPars->fVerbose )
     {
-        printf( "AIG object is %d bytes.  ", sizeof(Amap_Obj_t) );
+        printf( "AIG object is %d bytes.  ", (int)sizeof(Amap_Obj_t) );
         printf( "Internal AIG = %5.2f Mb.  Cuts = %5.2f Mb.\n", 
             1.0*Amap_ManObjNum(p)*sizeof(Amap_Obj_t)/(1<<20), 1.0*p->nBytesUsed/(1<<20) );
         printf( "Node =%6d. Try =%9d. Try3 =%10d. Used =%7d. R =%6.2f.  ", 
diff --git a/src/map/amap/amapRule.c b/src/map/amap/amapRule.c
index 0f6c7708..e8cb48c4 100644
--- a/src/map/amap/amapRule.c
+++ b/src/map/amap/amapRule.c
@@ -338,7 +338,7 @@ void Amap_LibCreateRules( Amap_Lib_t * pLib, int fVeryVerbose )
 {
     Amap_Gat_t * pGate;
     int i, nGates = 0;
-    int clk = clock();
+//    int clk = clock();
     pLib->fVerbose = fVeryVerbose;
     pLib->vRules   = Vec_PtrAlloc( 100 );
     pLib->vRulesX  = Vec_PtrAlloc( 100 );
diff --git a/src/map/cov/covCore.c b/src/map/cov/covCore.c
index b128ed65..f40e908a 100644
--- a/src/map/cov/covCore.c
+++ b/src/map/cov/covCore.c
@@ -250,8 +250,8 @@ void Abc_NtkCovCovers_rec( Cov_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundar
     Abc_NtkCovCovers_rec( p, pObj0, vBoundary );
     Abc_NtkCovCovers_rec( p, pObj1, vBoundary );
     // skip the node that spaced out
-    if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) ||  // fanin is not ready
-         !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) ||  // fanin is not ready
+    if ( (!pObj0->fMarkA && !Abc_ObjGetSupp(pObj0)) ||  // fanin is not ready
+         (!pObj1->fMarkA && !Abc_ObjGetSupp(pObj1)) ||  // fanin is not ready
          !Abc_NodeCovPropagate( p, pObj ) )           // node's support or covers cannot be computed
     {
         // save the nodes of the future boundary
diff --git a/src/map/if/ifDec07.c b/src/map/if/ifDec07.c
index 074ac6ef..8593d6ec 100644
--- a/src/map/if/ifDec07.c
+++ b/src/map/if/ifDec07.c
@@ -58,13 +58,13 @@ static word Truth6[6] = {
     0xFFFFFFFF00000000
 };
 static word Truth7[7][2] = {
-    0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
-    0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
-    0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
-    0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
-    0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
-    0xFFFFFFFF00000000,0xFFFFFFFF00000000,
-    0x0000000000000000,0xFFFFFFFFFFFFFFFF
+    {0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA},
+    {0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC},
+    {0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0},
+    {0xFF00FF00FF00FF00,0xFF00FF00FF00FF00},
+    {0xFFFF0000FFFF0000,0xFFFF0000FFFF0000},
+    {0xFFFFFFFF00000000,0xFFFFFFFF00000000},
+    {0x0000000000000000,0xFFFFFFFFFFFFFFFF}
 };
 
 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
@@ -82,20 +82,20 @@ void If_DecPrintConfig( word z )
    printf( " " );
    Kit_DsdPrintFromTruth( S, 4 );
    printf( " " );
-   printf( " %d", (z >> 16) & 7 );
-   printf( " %d", (z >> 20) & 7 );
-   printf( " %d", (z >> 24) & 7 );
-   printf( " %d", (z >> 28) & 7 );
+   printf( " %d", (int)((z >> 16) & 7) );
+   printf( " %d", (int)((z >> 20) & 7) );
+   printf( " %d", (int)((z >> 24) & 7) );
+   printf( " %d", (int)((z >> 28) & 7) );
    printf( "   " );
    S[0] = ((z >> 32) & 0xffff) | (((z >> 32) & 0xffff) << 16);
    Extra_PrintBinary( stdout, S, 16 );
    printf( " " );
    Kit_DsdPrintFromTruth( S, 4 );
    printf( " " );
-   printf( " %d", (z >> 48) & 7 );
-   printf( " %d", (z >> 52) & 7 );
-   printf( " %d", (z >> 56) & 7 );
-   printf( " %d", (z >> 60) & 7 );
+   printf( " %d", (int)((z >> 48) & 7) );
+   printf( " %d", (int)((z >> 52) & 7) );
+   printf( " %d", (int)((z >> 56) & 7) );
+   printf( " %d", (int)((z >> 60) & 7) );
    printf( "\n" );
 }
 
diff --git a/src/map/if/ifDec08.c b/src/map/if/ifDec08.c
index 54eff63e..15d26abf 100644
--- a/src/map/if/ifDec08.c
+++ b/src/map/if/ifDec08.c
@@ -58,16 +58,16 @@ static word Truth6[6] = {
     0xFFFFFFFF00000000
 };
 static word Truth10[10][16] = {
-    0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
-    0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
-    0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
-    0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
-    0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
-    0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,
-    0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF
+    {0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA},
+    {0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC},
+    {0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0},
+    {0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00},
+    {0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000},
+    {0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000},
+    {0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF},
+    {0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF},
+    {0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF},
+    {0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF}
 };
 
 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
@@ -481,7 +481,7 @@ printf( "\n" );
 int If_CutPerformCheck08( 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 <= 5 )
         return 1;
     If_Dec08Copy( pF, (word *)pTruth, nVars );
diff --git a/src/map/if/ifDec10.c b/src/map/if/ifDec10.c
index 01aa32ae..85c8625d 100644
--- a/src/map/if/ifDec10.c
+++ b/src/map/if/ifDec10.c
@@ -58,16 +58,16 @@ static word Truth6[6] = {
     0xFFFFFFFF00000000
 };
 static word Truth10[10][16] = {
-    0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
-    0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
-    0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
-    0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
-    0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
-    0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,
-    0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF
+    {0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA},
+    {0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC},
+    {0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0},
+    {0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00},
+    {0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000},
+    {0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000},
+    {0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF},
+    {0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF},
+    {0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF},
+    {0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF}
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c
index c1e87aaa..e624f889 100644
--- a/src/map/if/ifDec16.c
+++ b/src/map/if/ifDec16.c
@@ -53,17 +53,6 @@ struct If_Hte_t_
     word       pTruth[1];
 };
 
-// the bit count for the first 256 integer numbers
-static int BitCount8[256] = {
-    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
-    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
-    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
-    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
-};
 // variable swapping code
 static word PMasks[5][3] = {
     { 0x9999999999999999, 0x2222222222222222, 0x4444444444444444 },
@@ -657,14 +646,14 @@ void If_CluVerify( word * pF, int nVars, If_Grp_t * g, If_Grp_t * r, word BStrut
         If_CluInitTruthTables();
 
     for ( i = 0; i < g->nVars; i++ )
-        If_CluCopy( pTTFans[i], TruthAll[g->pVars[i]], nVars );
+        If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars );
     If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire );
 
     for ( i = 0; i < r->nVars; i++ )
         if ( r->pVars[i] == nVars )
             If_CluCopy( pTTFans[i], pTTWire, nVars );
         else
-            If_CluCopy( pTTFans[i], TruthAll[r->pVars[i]], nVars );
+            If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars );
     If_CluComposeLut( nVars, r, pFStruth, pTTFans, pTTRes );
 
     if ( !If_CluEqual(pTTRes, pF, nVars) )
@@ -690,11 +679,11 @@ void If_CluVerify3( word * pF, int nVars, If_Grp_t * g, If_Grp_t * g2, If_Grp_t
         If_CluInitTruthTables();
 
     for ( i = 0; i < g->nVars; i++ )
-        If_CluCopy( pTTFans[i], TruthAll[g->pVars[i]], nVars );
+        If_CluCopy( pTTFans[i], TruthAll[(int)g->pVars[i]], nVars );
     If_CluComposeLut( nVars, g, &BStruth, pTTFans, pTTWire );
 
     for ( i = 0; i < g2->nVars; i++ )
-        If_CluCopy( pTTFans[i], TruthAll[g2->pVars[i]], nVars );
+        If_CluCopy( pTTFans[i], TruthAll[(int)g2->pVars[i]], nVars );
     If_CluComposeLut( nVars, g2, &BStruth2, pTTFans, pTTWire2 );
 
     for ( i = 0; i < r->nVars; i++ )
@@ -703,7 +692,7 @@ void If_CluVerify3( word * pF, int nVars, If_Grp_t * g, If_Grp_t * g2, If_Grp_t
         else if ( r->pVars[i] == nVars + 1 )
             If_CluCopy( pTTFans[i], pTTWire2, nVars );
         else
-            If_CluCopy( pTTFans[i], TruthAll[r->pVars[i]], nVars );
+            If_CluCopy( pTTFans[i], TruthAll[(int)r->pVars[i]], nVars );
     If_CluComposeLut( nVars, r, &FStruth, pTTFans, pTTRes );
 
     if ( !If_CluEqual(pTTRes, pF, nVars) )
@@ -1293,7 +1282,7 @@ int If_CluCheckNonDisjointGroup( word * pF, int nVars, int * V2P, int * P2V, If_
         // try cofactoring w.r.t. each variable
         for ( v = 0; v < g->nVars; v++ )
         {
-            If_CluCofactors( pF, nVars, V2P[g->pVars[v]], pCofs[0], pCofs[1] );
+            If_CluCofactors( pF, nVars, V2P[(int)g->pVars[v]], pCofs[0], pCofs[1] );
             nCofsBest2 = If_CluCountCofs( pCofs[0], nVars, g->nVars, 0, NULL );
             if ( nCofsBest2 > 2 )
                 continue;
@@ -1316,7 +1305,7 @@ If_Grp_t If_CluFindGroup( word * pF, int nVars, int iVarStart, int * V2P, int *
 {
     int fVerbose = 0;
     int nRounds = 2;//nBSsize;
-    If_Grp_t G = {0}, * g = &G, BestG = {0};
+    If_Grp_t G = {0}, * g = &G;//, BestG = {0};
     int i, r, v, nCofs, VarBest, nCofsBest2;
     assert( nVars > nBSsize && nVars >= nBSsize + iVarStart && nVars <= CLU_VAR_MAX );
     assert( nBSsize >= 2 && nBSsize <= 6 );
@@ -1882,7 +1871,7 @@ If_Grp_t If_CluCheck3( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, in
     for ( i = 0; i < G2.nVars; i++ )
     {
         assert( G2.pVars[i] < R2.nVars );
-        G2.pVars[i] = R2.pVars[ G2.pVars[i] ];
+        G2.pVars[i] = R2.pVars[ (int)G2.pVars[i] ];
     }
     // remap variables
     for ( i = 0; i < R.nVars; i++ )
@@ -1890,7 +1879,7 @@ If_Grp_t If_CluCheck3( If_Man_t * p, word * pTruth0, int nVars, int nLutLeaf, in
         if ( R.pVars[i] == R2.nVars )
             R.pVars[i] = nVars + 1;
         else
-            R.pVars[i] = R2.pVars[ R.pVars[i] ];
+            R.pVars[i] = R2.pVars[ (int)R.pVars[i] ];
     }
 
     // decomposition exist
@@ -1940,7 +1929,7 @@ float If_CluDelayMax( If_Grp_t * g, float * pDelays )
     float Delay = 0.0;
     int i;
     for ( i = 0; i < g->nVars; i++ )
-        Delay = Abc_MaxFloat( Delay, pDelays[g->pVars[i]] );
+        Delay = Abc_MaxFloat( Delay, pDelays[(int)g->pVars[i]] );
     return Delay;
 }
 
@@ -2008,16 +1997,16 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
 
     // mark used groups
     for ( i = 0; i < G1.nVars; i++ )
-        fUsed[G1.pVars[i]] = 1;
+        fUsed[(int)G1.pVars[i]] = 1;
     for ( i = 0; i < G2.nVars; i++ )
-        fUsed[G2.pVars[i]] = 1;
+        fUsed[(int)G2.pVars[i]] = 1;
     // mark unused groups
     assert( G1.nMyu >= 2 && G1.nMyu <= 4 );
     if ( G1.nMyu > 2 )
-        fUsed[G1.pVars[G1.nVars-1]] = 0;
+        fUsed[(int)G1.pVars[G1.nVars-1]] = 0;
     assert( !G2.nVars || (G2.nMyu >= 2 && G2.nMyu <= 4) );
     if ( G2.nMyu > 2 )
-        fUsed[G2.pVars[G2.nVars-1]] = 0;
+        fUsed[(int)G2.pVars[G2.nVars-1]] = 0;
 
     // create remaining group
     assert( G3.nVars == 0 );
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index 8b5808d5..eaa33e92 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -198,7 +198,7 @@ int If_ManBinarySearchPeriod( If_Man_t * p )
 {
     If_Obj_t * pObj;
     int i, c, fConverged;
-    int fResetRefs = 0;
+//    int fResetRefs = 0;
     p->nAttempts++;
 
     // reset initial LValues (PIs to 0; others to -inf)
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index b5e2a3d0..b2687a77 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -53,7 +53,7 @@ word If_AndVerifyArray( Vec_Wrd_t * vAnds, int nVars )
 {
     Vec_Wrd_t * vTruths;
     If_And_t This;
-    word Entry, Truth0, Truth1, TruthR;
+    word Entry, Truth0, Truth1, TruthR = 0;
     int i;
     static word Truth[8] = {
         0xAAAAAAAAAAAAAAAA,
diff --git a/src/map/mapper/mapperSuper.c b/src/map/mapper/mapperSuper.c
index 7ade52fe..bd24552d 100644
--- a/src/map/mapper/mapperSuper.c
+++ b/src/map/mapper/mapperSuper.c
@@ -87,6 +87,7 @@ int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile )
     char * pLibName;
     int nCounter, nGatesTotal;
     unsigned uCanon[2];
+    int RetValue;
 
     // skip empty and comment lines
     while ( fgets( pBuffer, 2000, pFile ) != NULL )
@@ -122,7 +123,7 @@ int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile )
     }
 
     // read the number of variables
-    fscanf( pFile, "%d\n", &pLib->nVarsMax );
+    RetValue = fscanf( pFile, "%d\n", &pLib->nVarsMax );
     if ( pLib->nVarsMax < 2 || pLib->nVarsMax > 10 )
     {
         printf( "Suspicious number of variables (%d).\n", pLib->nVarsMax );
@@ -130,7 +131,7 @@ int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile )
     }
 
     // read the number of gates
-    fscanf( pFile, "%d\n", &nGatesTotal );
+    RetValue = fscanf( pFile, "%d\n", &nGatesTotal );
     if ( nGatesTotal < 1 || nGatesTotal > 10000000 )
     {
         printf( "Suspicious number of gates (%d).\n", nGatesTotal );
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index bfca980b..542ff258 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -114,6 +114,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     Map_Super_t * pGate;
     char * pTemp = 0, * pLibName;
     int nCounter, k, i;
+    int RetValue;
 
     // skip empty and comment lines
     while ( fgets( pBuffer, 5000, pFile ) != NULL )
@@ -177,7 +178,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     }
 
     // read the number of variables
-    fscanf( pFile, "%d\n", &pLib->nVarsMax );
+    RetValue = fscanf( pFile, "%d\n", &pLib->nVarsMax );
     if ( pLib->nVarsMax < 2 || pLib->nVarsMax > 10 )
     {
         printf( "Suspicious number of variables (%d).\n", pLib->nVarsMax );
@@ -185,7 +186,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     }
 
     // read the number of gates
-    fscanf( pFile, "%d\n", &pLib->nSupersReal );
+    RetValue = fscanf( pFile, "%d\n", &pLib->nSupersReal );
     if ( pLib->nSupersReal < 1 || pLib->nSupersReal > 10000000 )
     {
         printf( "Suspicious number of gates (%d).\n", pLib->nSupersReal );
@@ -193,7 +194,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     }
 
     // read the number of lines
-    fscanf( pFile, "%d\n", &pLib->nLines );
+    RetValue = fscanf( pFile, "%d\n", &pLib->nLines );
     if ( pLib->nLines < 1 || pLib->nLines > 10000000 )
     {
         printf( "Suspicious number of lines (%d).\n", pLib->nLines );
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 4512572d..a5f987e3 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1781,7 +1781,7 @@ DdNode * extraBddChangePolarity(
     if ( Cudd_IsConstant(bFunc) )
         return bFunc;
 
-    if ( bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars) )
+    if ( (bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars)) )
         return bRes;
     else
     {
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index 37ea9321..fe8b25f1 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -399,7 +399,7 @@ double Extra_CpuTimeDouble()
 ***********************************************************************/
 void Extra_MemTest()
 {
-    ABC_ALLOC( char, 1002 );
+//    ABC_ALLOC( char, 1002 );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilFile.c b/src/misc/util/utilFile.c
index 69d84c29..a25c5b2c 100644
--- a/src/misc/util/utilFile.c
+++ b/src/misc/util/utilFile.c
@@ -68,6 +68,8 @@ static ABC_UINT64_T realTimeAbs()  // -- absolute time in nano-seconds
 
     ok = QueryPerformanceCounter(&t); assert(ok);
     return (ABC_UINT64_T)(__int64)(((__int64)(((ABC_UINT64_T)t.LowPart | ((ABC_UINT64_T)t.HighPart << 32))) * realTime_freq * 1000000000));
+#else
+    return 0;
 #endif
 }
 
diff --git a/src/opt/cgt/cgtAig.c b/src/opt/cgt/cgtAig.c
index 757ebb85..b2cfd36f 100644
--- a/src/opt/cgt/cgtAig.c
+++ b/src/opt/cgt/cgtAig.c
@@ -90,7 +90,7 @@ void Cgt_ManDetectCandidates( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nLevelMax,
 void Cgt_ManDetectFanout_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout )
 {
     Aig_Obj_t * pFanout;
-    int f, iFanout;
+    int f, iFanout = -1;
     if ( Aig_ObjIsPo(pObj) || Aig_ObjLevel(pObj) > nOdcMax )
         return;
     if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
@@ -115,7 +115,7 @@ void Cgt_ManDetectFanout_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, V
 void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_Ptr_t * vFanout )
 {
     Aig_Obj_t * pFanout;
-    int i, k, f, iFanout;
+    int i, k, f, iFanout = -1;
     // collect visited nodes
     Vec_PtrClear( vFanout );
     Aig_ManIncrementTravId( pAig );
diff --git a/src/opt/cgt/cgtCore.c b/src/opt/cgt/cgtCore.c
index 958080c9..27810e1a 100644
--- a/src/opt/cgt/cgtCore.c
+++ b/src/opt/cgt/cgtCore.c
@@ -286,7 +286,7 @@ Aig_Man_t * Cgt_ClockGating( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pP
     Aig_Man_t * pGated;
     Vec_Vec_t * vGatesAll;
     Vec_Vec_t * vGates;
-    int nNodesUsed, clk = clock();
+    int nNodesUsed;//, clk = clock();
     vGatesAll = Cgt_ClockGatingCandidates( pAig, pCare, pPars );
     if ( pPars->fAreaOnly )
         vGates = Cgt_ManDecideArea( pAig, vGatesAll, pPars->nOdcMax, pPars->fVerbose );
diff --git a/src/opt/cgt/cgtDecide.c b/src/opt/cgt/cgtDecide.c
index 293bde85..2ac206cb 100644
--- a/src/opt/cgt/cgtDecide.c
+++ b/src/opt/cgt/cgtDecide.c
@@ -52,7 +52,7 @@ extern int Ssw_SmlNodeCountOnesRealVec( Ssw_Sml_t * p, Vec_Ptr_t * vObjs );
 void Cgt_ManCollectFanoutPos_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vFanout )
 {
     Aig_Obj_t * pFanout;
-    int f, iFanout;
+    int f, iFanout = -1;
     if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(pAig, pObj);
diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c
index 6ca3082d..adc41035 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -84,7 +84,7 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
     Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
     int clk = 0, clkStart, Counter = 0;
-    int nMffcSize, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
+    int nMffcSize;//, nMffcGains[MAX_VAL+1][MAX_VAL+1] = {{0}};
     // prepare the library
     Dar_LibPrepare( pPars->nSubgMax ); 
     // create rewriting manager
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c
index 2d047404..41794d18 100644
--- a/src/opt/dar/darLib.c
+++ b/src/opt/dar/darLib.c
@@ -1186,7 +1186,7 @@ int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKee
     int p_LevelBest  =  1000000;
     int p_GainBest   = -1000000;
     int p_ClassBest  = -1;
-    int fTraining    =  0;
+//    int fTraining    =  0;
     Dar_LibObj_t * pObj;
     int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
     clk = clock();
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index 79d6dfc4..5561908d 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -867,7 +867,7 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
     extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
 //    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
     extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-    int fVerbose = pPars->fVerbose;
+//    int fVerbose = pPars->fVerbose;
     Aig_Man_t * pMan, * pTemp;
     Gia_Man_t * pGia;
     Vec_Ptr_t * vPios;
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 51f05b21..b49b0bf3 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -391,10 +391,6 @@ p->timeCuts += clock() - clk;
     p->nCutsUseful += p->nEvals;
     for ( i = 0; i < p->nEvals; i++ )
     {
-        if ( p->pObj->Id == 1478 )
-        {
-            int x = 0;
-        }
         // get the cut
         pCut = p->pCuts + p->pEvals[i];
         if ( p->pPars->fFirst && i == 1 )
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 45f75674..e908a56c 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -102,7 +102,7 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
 {
     int fVeryVerbose = 0;
     unsigned * pData;
-    int RetValue, RetValue2 = -1, iVar, i, clk = clock();
+    int RetValue, RetValue2 = -1, iVar, i;//, clk = clock();
 /*
     if ( p->pPars->fGiaSat )
     {
diff --git a/src/opt/nwk/nwkMap.c b/src/opt/nwk/nwkMap.c
index 61ee50e8..cb35fee9 100644
--- a/src/opt/nwk/nwkMap.c
+++ b/src/opt/nwk/nwkMap.c
@@ -104,7 +104,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
 {
     extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
     Vec_Int_t * vSwitching = NULL, * vSwitching2 = NULL;
-    float * pSwitching, * pSwitching2;
+    float * pSwitching = NULL, * pSwitching2 = NULL;
     If_Man_t * pIfMan;
     If_Obj_t * pIfObj;
     Aig_Obj_t * pNode, * pFanin, * pPrev;
diff --git a/src/opt/nwk/nwkMerge.c b/src/opt/nwk/nwkMerge.c
index fa9f7c78..2a43bc16 100644
--- a/src/opt/nwk/nwkMerge.c
+++ b/src/opt/nwk/nwkMerge.c
@@ -677,9 +677,10 @@ Nwk_Grf_t * Nwk_ManLutMergeReadGraph( char * pFileName )
     FILE * pFile;
     char Buffer[100];
     int nNodes, nEdges, iNode1, iNode2;
+    int RetValue;
     pFile = fopen( pFileName, "r" );
-    fscanf( pFile, "%s %d", Buffer, &nNodes );
-    fscanf( pFile, "%s %d", Buffer, &nEdges );
+    RetValue = fscanf( pFile, "%s %d", Buffer, &nNodes );
+    RetValue = fscanf( pFile, "%s %d", Buffer, &nEdges );
     p = Nwk_ManGraphAlloc( nNodes );
     while ( fscanf( pFile, "%s %d %d", Buffer, &iNode1, &iNode2 ) == 3 )
         Nwk_ManGraphHashEdge( p, iNode1, iNode2 );
diff --git a/src/opt/rwr/rwrTemp.c b/src/opt/rwr/rwrTemp.c
index 6a670c3a..b32709e5 100644
--- a/src/opt/rwr/rwrTemp.c
+++ b/src/opt/rwr/rwrTemp.c
@@ -80,7 +80,7 @@ void Rwr_Temp()
     pFile = fopen( "nnclass_stats5.txt", "r" );
     for ( i = 0; i < 13719; i++ )
     {
-        fscanf( pFile, "%s%d", Buffer, &pFreqs[i] );
+        int RetValue = fscanf( pFile, "%s%d", Buffer, &pFreqs[i] );
         Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
         pTruths[i] = uTruth;
     }
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 );
diff --git a/src/sat/bsat/satChecker.c b/src/sat/bsat/satChecker.c
index 7aec4a4d..f478928c 100644
--- a/src/sat/bsat/satChecker.c
+++ b/src/sat/bsat/satChecker.c
@@ -121,6 +121,7 @@ void Sat_ProofChecker( char * pFileName )
     FILE * pFile;
     Vec_Vec_t * vClauses;
     int c, i, Num, RetValue, Counter, Counter2, Clause1, Clause2;
+    int RetValue;
     // open the file
     pFile = fopen( pFileName, "r" );
     if ( pFile == NULL )
@@ -138,7 +139,7 @@ void Sat_ProofChecker( char * pFileName )
     rewind( pFile );
     for ( i = 1 ; ; i++ )
     {
-        RetValue = fscanf( pFile, "%d", &Num );
+        RetValue = RetValue = fscanf( pFile, "%d", &Num );
         if ( RetValue != 1 )
             break;
         assert( Num == i );
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 81adb18b..223c830b 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -524,7 +524,7 @@ void Sat_ProofCheck( sat_solver2 * s )
     Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots;
     Vec_Set_t * vResolves;
     Vec_Int_t * vUsed, * vTemp;
-    satset * pSet, * pSet0, * pSet1;
+    satset * pSet, * pSet0 = NULL, * pSet1;
     int i, k, hRoot, Handle, Counter = 0, clk = clock(); 
     hRoot = s->hProofLast;
     if ( hRoot == -1 )
@@ -537,6 +537,7 @@ void Sat_ProofCheck( sat_solver2 * s )
     vResolves = Vec_SetAlloc();
     Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
     {
+        Handle = -1;
         pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
         for ( k = 1; k < (int)pSet->nEnts; k++ )
         {
@@ -578,7 +579,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_
 {
     Vec_Int_t * vCore;
     satset * pNode, * pFanin;
-    int i, k, clk = clock();
+    int i, k;//, clk = clock();
     vCore = Vec_IntAlloc( 1000 );
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
@@ -669,7 +670,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
     Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap;
     satset * pNode, * pFanin;
     Aig_Man_t * pAig;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj = NULL;
     int i, k, iVar, Lit, Entry, hRoot;
 //    if ( s->hLearntLast < 0 )
 //        return NULL;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 181d152a..1f86f2d3 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -257,9 +257,9 @@ static inline void act_var_rescale(sat_solver* s)  {
     s->var_inc *= 1e-100;
 }
 static inline void act_clause_rescale(sat_solver* s) {
-    static int Total = 0;
+//    static int Total = 0;
     clause** cs = (clause**)veci_begin(&s->learnts);
-    int i, clk = clock();
+    int i;//, clk = clock();
     for (i = 0; i < veci_size(&s->learnts); i++){
         float a = clause_activity(cs[i]);
         clause_setactivity(cs[i], a * (float)1e-20);
@@ -1300,8 +1300,8 @@ void luby_test()
 
 static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
 {
-    double  var_decay       = 0.95;
-    double  clause_decay    = 0.999;
+//    double  var_decay       = 0.95;
+//    double  clause_decay    = 0.999;
     double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
 
     ABC_INT64_T  conflictC       = 0;
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index a58cf22b..a02ecc3f 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1402,8 +1402,8 @@ void sat_solver2_reducedb(sat_solver2* s)
     satset * c, * pivot;
     cla h,* pArray,* pArray2;
     int * pPerm, * pClaAct, nClaAct, ActCutOff;
-    int i, j, k, hTemp, hHandle, clk = clock();
-    int Counter, CounterStart, LastSize;
+    int i, j, k, hTemp, hHandle, LastSize = 0;
+    int Counter, CounterStart, clk = clock();
 
     // check if it is time to reduce
     if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax )
@@ -1483,7 +1483,7 @@ void sat_solver2_reducedb(sat_solver2* s)
         }
     // compact clauses
     pivot = satset_read( &s->learnts, s->hLearntPivot );
-    s->hLearntPivot = hHandle;
+    s->hLearntPivot = hTemp = hHandle;
     satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i )
     {
         hTemp = c->Id; c->Id = i + 1;
@@ -1631,7 +1631,7 @@ int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose )
             if ( (pArray[k] >> 1) == Hand )
             {
                 if ( fVerbose )
-                printf( "Clause found in list %d at position.\n", i, k );
+                printf( "Clause found in list %d at position %d.\n", i, k );
                 Found = 1;
                 break;
             }
diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c
index 6ec2b6a6..840c923e 100644
--- a/src/sat/cnf/cnfFast.c
+++ b/src/sat/cnf/cnfFast.c
@@ -666,7 +666,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
 Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
 {
     Cnf_Dat_t * pCnf = NULL;
-    int clk, clkTotal = clock();
+    int clk;//, clkTotal = clock();
 //    printf( "\n" );
     Aig_ManCleanMarkAB( p );
     // create initial marking
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 2904607f..61c4d4d3 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -282,8 +282,12 @@ 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))) ) &&
-        Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(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) )
+        );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index 3312c23d..4ef40ad0 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -111,11 +111,11 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
 {
     printf("C solver (%d vars; %d clauses; %d learned):\n", 
         p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
-    printf("starts        : %lld\n", p->Stats.nStarts);
-    printf("conflicts     : %lld\n", p->Stats.nConflicts);
-    printf("decisions     : %lld\n", p->Stats.nDecisions);
-    printf("propagations  : %lld\n", p->Stats.nPropagations);
-    printf("inspects      : %lld\n", p->Stats.nInspects);
+    printf("starts        : %d\n", (int)p->Stats.nStarts);
+    printf("conflicts     : %d\n", (int)p->Stats.nConflicts);
+    printf("decisions     : %d\n", (int)p->Stats.nDecisions);
+    printf("propagations  : %d\n", (int)p->Stats.nPropagations);
+    printf("inspects      : %d\n", (int)p->Stats.nInspects);
 }
 
 /**Function*************************************************************