Fixed a number of small bugs and memory leaks.

51 files changed, 130 insertions, 50 deletions

diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index e31ab74b..549da741 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -400,7 +400,7 @@ Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
     Aig_ManForEachPiSeq( p, pObj, i )
         Vec_PtrPush( vMap, pObj );
     // create mapping of fanin nodes into the corresponding latch outputs
-    pMapping = ABC_ALLOC( int, 2 * Aig_ManObjNumMax(p) );
+    pMapping = ABC_FALLOC( int, 2 * Aig_ManObjNumMax(p) );
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
     {
         pFanin = Aig_ObjFanin0(pObjLi);
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 1b97fb2c..1ce181ea 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -731,6 +731,7 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
     printf( "\n" );
+    Vec_PtrFree( vNodes );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index ef355992..9c6dced3 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -245,7 +245,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     DdNode * bNext = NULL; // Suppress "might be used uninitialized"
     DdNode * bTemp;
     Cudd_ReorderingType method;
-    int i, nIters, nBddSize, status;
+    int i, nIters, nBddSize = 0, status;
     int nThreshold = 10000, clk = clock();
     Vec_Ptr_t * vOnionRings;
 
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index 97f5e36a..7d59515e 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
 Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
 {
     Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj, * pRepr;
+    Gia_Obj_t * pObj, * pRepr = NULL;
     int iRes0, iRes1, iRepr, iNode, iMiter;
     int i, fCompl, * piCopies, * pDepths;
     Gia_ManSetPhase( p->pAig );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 9b1ad3f2..8cf2a54d 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -281,8 +281,8 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
 
     // allocate the hash table hashing simulation info into nodes
     nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
-    ppTable = ABC_ALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = ABC_ALLOC( Aig_Obj_t *, nTableSize ); 
+    ppTable = ABC_FALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ABC_FALLOC( Aig_Obj_t *, nTableSize ); 
     memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
 
     // add all the nodes to the hash table
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 0e004f87..811a370b 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -331,7 +331,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
     Aig_Obj_t ** ppNodes;
     Gia_Obj_t * pObj;
     int i;
-    ppNodes = ABC_ALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
+    ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 07b81a86..14a2769e 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -365,8 +365,8 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
     // check if the input file format is correct
     if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
     {
+        ABC_FREE( pContents );
         fprintf( stdout, "Wrong input file format.\n" );
-        free( pContents );
         return NULL;
     }
 
@@ -385,6 +385,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
     // check the parameters
     if ( nTotal != nInputs + nLatches + nAnds )
     {
+        ABC_FREE( pContents );
         fprintf( stdout, "The paramters are wrong.\n" );
         return NULL;
     }
diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
index 6f1ce5a7..6eb20635 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -67,7 +67,7 @@ void Gia_ManFrontTransform( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i, * pFrontToId; // mapping of nodes into frontier variables
     assert( p->nFront > 0 );
-    pFrontToId = ABC_ALLOC( int, p->nFront );
+    pFrontToId = ABC_FALLOC( int, p->nFront );
     Gia_ManForEachObj( p, pObj, i )
     {
         if ( Gia_ObjIsCo(pObj) )
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index a06a6024..787aa090 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -262,10 +262,14 @@ int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars )
     vAigToIf = Vec_PtrStart( Gia_ManObjNum(p) );
     pIfMan = Gia_ManToIf( p, pPars, vAigToIf );    
     if ( pIfMan == NULL )
+    {
+        Vec_PtrFree( vAigToIf );
         return 0;
+    }
 //    pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
     if ( !If_ManPerformMapping( pIfMan ) )
     {
+        Vec_PtrFree( vAigToIf );
         If_ManStop( pIfMan );
         return 0;
     }
diff --git a/src/aig/gia/giaPat.c b/src/aig/gia/giaPat.c
index bd43380f..643ae6b7 100644
--- a/src/aig/gia/giaPat.c
+++ b/src/aig/gia/giaPat.c
@@ -113,6 +113,7 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V
         Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
         Sat_ObjSetXValue( pObj, Value );
     }
+    Value = Sat_ObjXValue( Gia_ObjFanin0(pRoot) );
     Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pRoot) );
     if ( Value != GIA_ONE )
         printf( "Gia_SatVerifyPattern(): Verification FAILED.\n" );
diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c
index 76ed7b17..17578f06 100644
--- a/src/aig/hop/hopUtil.c
+++ b/src/aig/hop/hopUtil.c
@@ -492,6 +492,7 @@ void Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig )
     Vec_PtrForEachEntry( Hop_Obj_t *, vNodes, pObj, i )
         Hop_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
     printf( "\n" );
+    Vec_PtrFree( vNodes );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
index defaa752..096e82e4 100644
--- a/src/aig/ioa/ioaReadAig.c
+++ b/src/aig/ioa/ioaReadAig.c
@@ -116,7 +116,6 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
     if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
     {
         fprintf( stdout, "Wrong input file format.\n" );
-        free( pContents );
         return NULL;
     }
 
diff --git a/src/aig/ivy/ivyUtil.c b/src/aig/ivy/ivyUtil.c
index 4df67517..c8d4003a 100644
--- a/src/aig/ivy/ivyUtil.c
+++ b/src/aig/ivy/ivyUtil.c
@@ -732,6 +732,7 @@ void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" );
     printf( "\n" );
+    Vec_IntFree( vNodes );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index d82ac71e..331cd906 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -243,8 +243,6 @@ void Ntl_ManPrepareCecMans( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, Aig_Man_t ** p
     Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
     if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) )
     {
-        if ( pMan1 )  Ntl_ManFree( pMan1 );
-        if ( pMan2 )  Ntl_ManFree( pMan2 );
         printf( "Ntl_ManPrepareCec(): Cannot verify designs with too many different CIs.\n" );
         return;
     }
@@ -253,8 +251,6 @@ void Ntl_ManPrepareCecMans( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, Aig_Man_t ** p
     if ( Vec_PtrSize(pMan1->vCos) == 0 )
     {
         printf( "Ntl_ManPrepareCec(): There is no identically-named primary outputs to compare.\n" );
-        if ( pMan1 )  Ntl_ManFree( pMan1 );
-        if ( pMan2 )  Ntl_ManFree( pMan2 );
         return;
     }
     // derive AIGs
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 103f8540..88962efa 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -444,6 +444,7 @@ static char * Ntl_ReadLoadFile( char * pFileName )
     pFile = fopen( pFileName, "rb" );
     if ( pFile == NULL )
     {
+        fclose( pFile );
         printf( "Ntl_ReadLoadFile(): The file is unavailable (absent or open).\n" );
         return NULL;
     }
@@ -451,6 +452,7 @@ static char * Ntl_ReadLoadFile( char * pFileName )
     nFileSize = ftell( pFile ); 
     if ( nFileSize == 0 )
     {
+        fclose( pFile );
         printf( "Ntl_ReadLoadFile(): The file is empty.\n" );
         return NULL;
     }
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 9c36deb3..8e537142 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -751,7 +751,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     Aig_Man_t * pNew;
     Cnf_Dat_t * pCnf;
     int nOutsSolved = 0;
-    int Iter, RetValue, clk = clock(), clk2, clkTotal = clock();
+    int Iter, RetValue = -1, clk = clock(), clk2, clkTotal = clock();
     int Status = -1;
 /*
     Vec_Ptr_t * vSimInfo;
@@ -801,9 +801,9 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         if ( nTimeOut && ((float)nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
         {
             printf( "Reached timeout (%d seconds).\n",  nTimeOut );
-            Saig_BmcManStop( p );
             if ( piFrames )
                 *piFrames = p->iFrameLast-1;
+            Saig_BmcManStop( p );
             return Status;
         }
     }
diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c
index b4024634..d58074e3 100644
--- a/src/aig/saig/saigConstr.c
+++ b/src/aig/saig/saigConstr.c
@@ -57,7 +57,11 @@ Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
     int i, RetValue;
     RetValue = Saig_ManDetectConstr( pAig, &vOuts, &vCons );
     if ( RetValue == 0 )
+    {
+        Vec_PtrFreeP( &vOuts );
+        Vec_PtrFreeP( &vCons );
         return Aig_ManDupDfs( pAig );
+    }
     // start the new manager
     pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
     pAigNew->pName = Aig_UtilStrsav( pAig->pName );
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index fad77020..1c288407 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -665,7 +665,7 @@ void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
 ***********************************************************************/
 int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
 {
-    int Values[257];
+    int Values[257] = {0};
     unsigned * pState;
     int r, i, k, Reg, Value;
     int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
diff --git a/src/aig/saig/saigWnd.c b/src/aig/saig/saigWnd.c
index eeacb44e..c11798ea 100644
--- a/src/aig/saig/saigWnd.c
+++ b/src/aig/saig/saigWnd.c
@@ -802,6 +802,8 @@ Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 )
     }
     Aig_ManSetRegNum( pNew, nRegCount );
     Aig_ManCleanup( pNew );
+    Vec_PtrFree( vNodes0 );
+    Vec_PtrFree( vNodes1 );
     return pNew;
 }
 
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 1419b889..76cc34fa 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -234,7 +234,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
 {
     int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
     Aig_Man_t * pAigNew;
-    int RetValue, nIter;
+    int RetValue, nIter = -1;
     int clk, clkTotal = clock();
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c
index 21535cb5..cffdc8da 100644
--- a/src/base/abc/abcBlifMv.c
+++ b/src/base/abc/abcBlifMv.c
@@ -228,11 +228,13 @@ int Abc_NodeStrashBlifMv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
             }
             if ( *pSop == '!' )
             {
+                ABC_FREE( pValues );
                 printf( "Abc_NodeStrashBlifMv(): Cannot handle complement in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
                 return 0;
             }
             if ( *pSop == '{' )
             {
+                ABC_FREE( pValues );
                 printf( "Abc_NodeStrashBlifMv(): Cannot handle braces in the MV function of node %s.\n", Abc_ObjName(Abc_ObjFanout0(pObj)) );
                 return 0;
             }
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 81990bac..7ff7db17 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -572,6 +572,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
         pNode->pData = Abc_ConvertSopToAig( pMan, (char *)pNode->pData );
         if ( pNode->pData == NULL )
         {
+            Hop_ManStop( pMan );
             printf( "Abc_NtkSopToAig: Error while converting SOP into AIG.\n" );
             return 0;
         }
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 2a4cf7d2..424f6bd1 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -900,6 +900,7 @@ char * Abc_SopFromTruthBin( char * pTruth )
             Digit = pTruth[i] - '0';
         else
         {
+            Vec_IntFree( vMints );
             printf( "String %s does not look like a binary representation of the truth table.\n", pTruth );
             return NULL;
         }
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index e063a238..1e5777b9 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1851,13 +1851,20 @@ void Abc_NtkCompareCones( Abc_Ntk_t * pNtk )
         printf( "%4d CO %5d :  Supp = %5d.  Lev = %3d.  Cone = %5d.  Rev = %5d.  COs = %3d (%3d).\n",
             Iter, pPerms[i], Vec_PtrSize(vSupp), Abc_ObjLevel(Abc_ObjFanin0(pObj)), Vec_PtrSize(vNodes), Counter, CounterCos, CounterCosNew );
 
+        if ( Vec_PtrSize(vSupp) < 10 )
+        {
+            // free arrays
+            Vec_PtrFree( vSupp );
+            Vec_PtrFree( vNodes );
+            Vec_PtrFree( vReverse );
+            break;
+        }
+
         // free arrays
         Vec_PtrFree( vSupp );
         Vec_PtrFree( vNodes );
         Vec_PtrFree( vReverse );
 
-        if ( Vec_PtrSize(vSupp) < 10 )
-            break;
     }
     Abc_NtkForEachCo( pNtk, pObj, i )
         pObj->fMarkA = 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8443ef83..b8c8f7a0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2103,7 +2103,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     // convert it to truth table
     {
         Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
-        Vec_Int_t * vMemory = Vec_IntAlloc(0);
+        Vec_Int_t * vMemory;
         unsigned * pTruth;
         if ( !Abc_ObjIsNode(pObj) )
         {
@@ -2115,6 +2115,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( -1, "Currently works only for up to 16 inputs.\n" );
             return 1;
         }
+        vMemory = Vec_IntAlloc(0);
         pTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, Hop_Regular((Hop_Obj_t *)pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
         if ( Hop_IsComplement((Hop_Obj_t *)pObj->pData) )
             Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
@@ -5581,7 +5582,7 @@ usage:
 int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
-    int fComb;
+    int fComb = 0;
     int c;
     extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
 
@@ -5656,7 +5657,7 @@ usage:
 int Abc_CommandAndPos( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);//, * pNtkRes;
-    int fComb;
+    int fComb = 0;
     int c;
 
     // set defaults
@@ -5932,7 +5933,7 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtk2;
     char * FileName;
-    int fComb;
+    int fComb = 0;
     int c;
     pNtk = Abc_FrameReadNtk(pAbc);
 
@@ -5972,6 +5973,7 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
     // check if the second network is combinational
     if ( Abc_NtkLatchNum(pNtk2) )
     {
+        Abc_NtkDelete( pNtk2 );
         Abc_Print( -1, "The second network has latches. Appending does not work for such networks.\n" );
         return 0;
     }
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 558d9349..250cac14 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -113,14 +113,15 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int
     // perform the decomposition
     dd = (DdManager *)Abc_NtkGlobalBddMan(pNtk);
     pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
-    Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
-    Vec_PtrFree( vFuncsGlob );
-    Abc_NtkFreeGlobalBdds( pNtk, 0 );
     if ( pManDsd == NULL )
     {
+        Vec_PtrFree( vFuncsGlob );
         Cudd_Quit( dd );
         return NULL;
     }
+    Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
+    Vec_PtrFree( vFuncsGlob );
+    Abc_NtkFreeGlobalBdds( pNtk, 0 );
 
     // start the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index acdfcd93..7a9a5239 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -1031,7 +1031,7 @@ int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
 {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
     Aig_Man_t * pMan;
-    int status, fStrashed = 0;
+    int status = 0, fStrashed = 0;
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtk = Abc_NtkStrash(pNtk, 0, 0, 0);
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 15cbdda5..35eb535a 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -671,7 +671,7 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv )
             }
             if ( interactive && *line != '\0' )
             {
-                Cmd_HistoryAddCommand( pAbc, Extra_UtilStrsav(line) );
+                Cmd_HistoryAddCommand( pAbc, line );
                 if ( pAbc->Hst != NULL )
                 {
                     fprintf( pAbc->Hst, "%s\n", line );
diff --git a/src/base/cmd/cmdLoad.c b/src/base/cmd/cmdLoad.c
index b96737c6..797275db 100644
--- a/src/base/cmd/cmdLoad.c
+++ b/src/base/cmd/cmdLoad.c
@@ -58,6 +58,7 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
     // check if there is the binary
     if ( (pFile = fopen( Vec_StrArray(vCommand), "r" )) == NULL )
     {
+        Vec_StrFree( vCommand );
         Abc_Print( -1, "Cannot run the binary \"%s\".\n\n", Vec_StrArray(vCommand) );
         return 1;
     }
@@ -73,10 +74,12 @@ int CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
     // run the command line
     if ( Util_SignalSystem( Vec_StrArray(vCommand) ) )
     {
+        Vec_StrFree( vCommand );
         Abc_Print( -1, "The following command has returned non-zero exit status:\n" );
         Abc_Print( -1, "\"%s\"\n", Vec_StrArray(vCommand) );
         return 1;
     }
+    Vec_StrFree( vCommand );
     return 0;
 }
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 46cbb33a..1230cd8e 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -933,6 +933,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
         pSopCover = Abc_SopFromTruthBin(argv[globalUtilOptind]);
     if ( pSopCover == NULL || pSopCover[0] == 0 )
     {
+        ABC_FREE( pSopCover );
         fprintf( pAbc->Err, "Reading truth table has failed.\n" );
         return 1;
     }
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index a1241354..9fd41261 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -149,9 +149,9 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
         if ( p->vTokens && strcmp((char *)p->vTokens->pArray[0], ".exdc") == 0 )
         {
             pNtk->pExdc = Io_ReadBlifNetworkOne( p );
-            Abc_NtkFinalizeRead( pNtk->pExdc );
             if ( pNtk->pExdc == NULL )
                 break;
+            Abc_NtkFinalizeRead( pNtk->pExdc );
         }
         // add this network as part of the hierarchy
         if ( pNtkMaster == NULL ) // no master network so far
diff --git a/src/base/io/ioReadBlifAig.c b/src/base/io/ioReadBlifAig.c
index caa776f9..1ef61196 100644
--- a/src/base/io/ioReadBlifAig.c
+++ b/src/base/io/ioReadBlifAig.c
@@ -444,6 +444,7 @@ static char * Io_BlifLoadFile( char * pFileName )
     nFileSize = ftell( pFile ); 
     if ( nFileSize == 0 )
     {
+        fclose( pFile );
         printf( "Io_BlifLoadFile(): The file is empty.\n" );
         return NULL;
     }
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index c3612b2d..1c28ac3d 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -538,6 +538,7 @@ static char * Io_MvLoadFile( char * pFileName )
     nFileSize = ftell( pFile ); 
     if ( nFileSize == 0 )
     {
+        fclose( pFile );
         printf( "Io_MvLoadFile(): The file is empty.\n" );
         return NULL;
     }
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 36d44c68..927cf7e5 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -120,6 +120,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
             printf( "%s (line %d): Wrong number of token.\n", 
                 Extra_FileReaderGetFileName(p), iLine+1 );
             Abc_NtkDelete( pNtk );
+            Extra_ProgressBarStop( pProgress );
+            ABC_FREE( ppSops );
             return NULL;
         }
 
@@ -152,6 +154,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
                 {
                     printf( "%s: The number of inputs is not specified.\n", Extra_FileReaderGetFileName(p) );
                     Abc_NtkDelete( pNtk );
+                    Extra_ProgressBarStop( pProgress );
+                    ABC_FREE( ppSops );
                     return NULL;
                 }
                 nDigits = Extra_Base10Log( nInputs );
@@ -167,6 +171,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
                 {
                     printf( "%s: The number of outputs is not specified.\n", Extra_FileReaderGetFileName(p) );
                     Abc_NtkDelete( pNtk );
+                    Extra_ProgressBarStop( pProgress );
+                    ABC_FREE( ppSops );
                     return NULL;
                 }
                 nDigits = Extra_Base10Log( nOutputs );
@@ -199,6 +205,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
                 printf( "%s (line %d): Input and output cubes are not specified.\n", 
                     Extra_FileReaderGetFileName(p), iLine+1 );
                 Abc_NtkDelete( pNtk );
+                Extra_ProgressBarStop( pProgress );
+                ABC_FREE( ppSops );
                 return NULL;
             }
             pCubeIn  = (char *)vTokens->pArray[0];
@@ -215,6 +223,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
                 printf( "%s (line %d): Output cube length (%zu) differs from the number of outputs (%d).\n",
                     Extra_FileReaderGetFileName(p), iLine+1, strlen(pCubeOut), nOutputs );
                 Abc_NtkDelete( pNtk );
+                Extra_ProgressBarStop( pProgress );
+                ABC_FREE( ppSops );
                 return NULL;
             }
             if ( fZeros )
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 3900cf26..1087af4f 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -668,6 +668,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
                 fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" );
                 fclose( b.f );
                 ABC_FREE(b.buf);
+                Vec_StrFree( vBinary );
                 return;
             }
         }
@@ -694,6 +695,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
             printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
             fclose( b.f );
             ABC_FREE(b.buf);
+            Extra_ProgressBarStop( pProgress );
             return;
         }
     }
diff --git a/src/base/io/ioWriteBook.c b/src/base/io/ioWriteBook.c
index 9d0df473..45807ce6 100644
--- a/src/base/io/ioWriteBook.c
+++ b/src/base/io/ioWriteBook.c
@@ -117,6 +117,7 @@ void Io_WriteBook( Abc_Ntk_t * pNtk, char * FileName )
         // write the aux file
     if ( (pFileNodes == NULL) || (pFileNets == NULL) || (pFileAux == NULL) )
     {
+        fclose( pFileAux );
         fprintf( stdout, "Io_WriteBook(): Cannot open the output files.\n" );
         return;
     }
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index bb7142f3..eb036620 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -109,7 +109,10 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
     p->pFileName = pFileName;
     p->pReader   = Ver_StreamAlloc( pFileName );
     if ( p->pReader == NULL )
+    {
+        ABC_FREE( p );
         return NULL;
+    }
     p->Output    = stdout;
     p->vNames    = Vec_PtrAlloc( 100 );
     p->vStackFn  = Vec_PtrAlloc( 100 );
@@ -2537,7 +2540,7 @@ int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBu
             Abc_ObjAddFanin( pNetAct, pTermNew );
         }
         // remove the bundle
-        Ver_ParseFreeBundle( pBundle );
+        Ver_ParseFreeBundle( pBundle ); pBundle = NULL;
         Vec_PtrWriteEntry( (Vec_Ptr_t *)pBox->pCopy, j, NULL );
     }
     ABC_FREE( pName );
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c
index 3b2e989d..c0cac4ec 100644
--- a/src/bdd/cudd/cuddExport.c
+++ b/src/bdd/cudd/cuddExport.c
@@ -780,6 +780,7 @@ Cudd_DumpDDcal(
         if (diff <= mask) break;
     }
     st_free_table(visited);
+    visited = NULL;
 
     /* Build a bit array with the support of f. */
     sorted = ABC_ALLOC(int,nvars);
@@ -851,7 +852,8 @@ Cudd_DumpDDcal(
     retval = fprintf(fp, "]\n");
     if (retval == EOF) goto failure;
 
-    st_free_table(visited);
+    if ( visited )
+        st_free_table(visited);
     return(1);
 
 failure:
diff --git a/src/bdd/parse/parseEqn.c b/src/bdd/parse/parseEqn.c
index 55b9c2f0..ed2599ca 100644
--- a/src/bdd/parse/parseEqn.c
+++ b/src/bdd/parse/parseEqn.c
@@ -184,6 +184,8 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
                     // perform the given operation
                     if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper ) == NULL )
                     {
+                        Parse_StackFnFree( pStackFn );
+                        Parse_StackOpFree( pStackOp );
                         fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
                         ABC_FREE( pFormula );
                         return NULL;
@@ -277,6 +279,8 @@ Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t
                     {
                         fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
                         ABC_FREE( pFormula );
+                        Parse_StackFnFree( pStackFn );
+                        Parse_StackOpFree( pStackOp );
                         return NULL;
                     }
                     Parse_StackOpPush( pStackOp,  Oper1 );     // push the last operation back
diff --git a/src/map/amap/amapParse.c b/src/map/amap/amapParse.c
index 3ebbec11..49c1eb66 100644
--- a/src/map/amap/amapParse.c
+++ b/src/map/amap/amapParse.c
@@ -235,6 +235,8 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     {
                         fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
                         ABC_FREE( pFormula );
+                        Vec_PtrFreeP( &pStackFn );
+                        Vec_IntFreeP( &pStackOp );
                         return NULL;
                     }
                 }
@@ -333,6 +335,8 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
                     {
                         fprintf( pOutput, "Amap_ParseFormula(): Unknown operation\n" );
                         ABC_FREE( pFormula );
+                        Vec_PtrFreeP( &pStackFn );
+                        Vec_IntFreeP( &pStackOp );
                         return NULL;
                     }
                     Vec_IntPush( pStackOp,  Oper1 );     // push the last operation back
@@ -354,10 +358,10 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
             if ( Vec_PtrSize(pStackFn) == 0 )
                 if ( Vec_IntSize( pStackOp ) == 0 )
                 {
-                    Vec_PtrFree(pStackFn);
-                    Vec_IntFree(pStackOp);
 //                    Cudd_Deref( gFunc );
                     ABC_FREE( pFormula );
+                    Vec_PtrFreeP( &pStackFn );
+                    Vec_IntFreeP( &pStackOp );
                     return gFunc;
                 }
                 else
@@ -369,6 +373,8 @@ Hop_Obj_t * Amap_ParseFormula( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVa
             fprintf( pOutput, "Amap_ParseFormula(): The input string is empty\n" );
     }
     ABC_FREE( pFormula );
+    Vec_PtrFreeP( &pStackFn );
+    Vec_IntFreeP( &pStackOp );
     return NULL;
 }
 
diff --git a/src/map/amap/amapRead.c b/src/map/amap/amapRead.c
index ec169773..77292099 100644
--- a/src/map/amap/amapRead.c
+++ b/src/map/amap/amapRead.c
@@ -331,6 +331,7 @@ Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
     {
         if ( strcmp( pToken, AMAP_STRING_GATE ) )
         {
+            Amap_LibFree( p );
             printf( "The first line should begin with %s.\n", AMAP_STRING_GATE );
             return NULL;
         }
@@ -358,6 +359,7 @@ Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
             pToken = (char *)Vec_PtrEntry(vTokens, iPos++);
             if ( strcmp( pToken, AMAP_STRING_PIN ) )
             {
+                Amap_LibFree( p );
                 printf( "Cannot parse gate %s.\n", pGate->pName );
                 return NULL;
             }
@@ -373,6 +375,7 @@ Amap_Lib_t * Amap_ParseTokens( Vec_Ptr_t * vTokens, int fVerbose )
                 pPin->Phase = AMAP_PHASE_NONINV;
             else 
             {
+                Amap_LibFree( p );
                 printf( "Cannot read phase of pin %s of gate %s\n", pPin->pName, pGate->pName );
                 return NULL;
             }
@@ -429,7 +432,10 @@ Amap_Lib_t * Amap_LibReadFile( char * pFileName, int fVerbose )
     vTokens = Amap_DeriveTokens( pBuffer );
     pLib = Amap_ParseTokens( vTokens, fVerbose );
     if ( pLib == NULL )
+    {
+        Vec_PtrFree( vTokens );
         return NULL;
+    }
     pLib->pName = Amap_ParseStrsav( pLib->pMemGates, pFileName );
     Vec_PtrFree( vTokens );
     ABC_FREE( pBuffer );
diff --git a/src/map/if/ifLib.c b/src/map/if/ifLib.c
index 90e37a0f..3822302e 100644
--- a/src/map/if/ifLib.c
+++ b/src/map/if/ifLib.c
@@ -73,6 +73,7 @@ If_Lib_t * If_LutLibRead( char * FileName )
         if ( i != atoi(pToken) )
         {
             Abc_Print( 1, "Error in the LUT library file \"%s\".\n", FileName );
+            ABC_FREE( p->pName );
             ABC_FREE( p );
             return NULL;
         }
@@ -89,6 +90,8 @@ If_Lib_t * If_LutLibRead( char * FileName )
         // check for out-of-bound
         if ( k > i )
         {
+            ABC_FREE( p->pName );
+            ABC_FREE( p );
             Abc_Print( 1, "LUT %d has too many pins (%d). Max allowed is %d.\n", i, k, i );
             return NULL;
         }
@@ -99,6 +102,8 @@ If_Lib_t * If_LutLibRead( char * FileName )
 
         if ( i == IF_MAX_LUTSIZE )
         {
+            ABC_FREE( p->pName );
+            ABC_FREE( p );
             Abc_Print( 1, "Skipping LUTs of size more than %d.\n", i );
             return NULL;
         }
diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c
index 9cc8747d..bd7f9b87 100644
--- a/src/map/mapper/mapperLib.c
+++ b/src/map/mapper/mapperLib.c
@@ -86,6 +86,7 @@ clk = clock();
     {
         if ( pExcludeFile != 0 )
         {
+            Map_SuperLibFree( p );
             printf ("Error: Exclude file support not present for old format. Stop.\n");
             return NULL;
         }
diff --git a/src/map/mapper/mapperMatch.c b/src/map/mapper/mapperMatch.c
index 19dd6939..6a2ad74a 100644
--- a/src/map/mapper/mapperMatch.c
+++ b/src/map/mapper/mapperMatch.c
@@ -93,16 +93,23 @@ int Map_MappingMatches( Map_Man_t * p )
         // make sure that at least one non-trival cut is present
         if ( pNode->pCuts->pNext == NULL )
         {
+            Extra_ProgressBarStop( pProgress );
             printf( "\nError: A node in the mapping graph does not have feasible cuts.\n" );
             return 0;
         }
 
         // match negative phase
         if ( !Map_MatchNodePhase( p, pNode, 0 ) )
+        {
+            Extra_ProgressBarStop( pProgress );
             return 0;
+        }
         // match positive phase
         if ( !Map_MatchNodePhase( p, pNode, 1 ) )
+        {
+            Extra_ProgressBarStop( pProgress );
             return 0;
+        }
 
         // make sure that at least one phase is mapped
         if ( pNode->pCutBest[0] == NULL && pNode->pCutBest[1] == NULL )
@@ -110,6 +117,7 @@ int Map_MappingMatches( Map_Man_t * p )
             printf( "\nError: Could not match both phases of AIG node %d.\n", pNode->Num );
             printf( "Please make sure that the supergate library has equivalents of AND2 or NAND2.\n" );
             printf( "If such supergates exist in the library, report a bug.\n" );
+            Extra_ProgressBarStop( pProgress );
             return 0;
         }
 
diff --git a/src/map/mapper/mapperSuper.c b/src/map/mapper/mapperSuper.c
index 3be70541..58deddb7 100644
--- a/src/map/mapper/mapperSuper.c
+++ b/src/map/mapper/mapperSuper.c
@@ -89,7 +89,7 @@ int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile )
     unsigned uCanon[2];
 
     // skip empty and comment lines
-    while ( fgets( pBuffer, 5000, pFile ) != NULL )
+    while ( fgets( pBuffer, 2000, pFile ) != NULL )
     {
         // skip leading spaces
         for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index eb5d47ea..3b93856c 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -65,7 +65,6 @@ Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFil
             tExcludeGate = 0;
             return 0;
         }
-       
         fprintf ( Abc_FrameReadOut( (Abc_Frame_t *)pAbc ), "Read %d gates from exclude file\n", num );
     }
 
@@ -76,6 +75,8 @@ Mio_Library_t * Mio_LibraryRead( void * pAbc, char * FileName, char * ExcludeFil
         if ( pLib != NULL )
             printf ( "Warning: Read extended GENLIB format but ignoring extensions\n" );
     }
+    if ( tExcludeGate )
+        st_free_table( tExcludeGate );
 
     return pLib;
 }
diff --git a/src/opt/cut/cutOracle.c b/src/opt/cut/cutOracle.c
index f7883e3f..b26e7d5e 100644
--- a/src/opt/cut/cutOracle.c
+++ b/src/opt/cut/cutOracle.c
@@ -126,9 +126,6 @@ Cut_Oracle_t * Cut_OracleStart( Cut_Man_t * pMan )
 ***********************************************************************/
 void Cut_OracleStop( Cut_Oracle_t * p )
 {
-    Cut_Cut_t * pCut;
-    int i;
-
 //    if ( p->pParams->fVerbose )
     {
         printf( "Cut computation statistics with oracle:\n" );
@@ -136,8 +133,6 @@ void Cut_OracleStop( Cut_Oracle_t * p )
         ABC_PRT( "Total time ", p->timeTotal );
     }
 
-    Vec_PtrForEachEntry( Cut_Cut_t *, p->vCutsNew, pCut, i )
-
     if ( p->vCuts0 )      Vec_PtrFree( p->vCuts0 );
     if ( p->vCuts1 )      Vec_PtrFree( p->vCuts1 );
     if ( p->vCutsNew )    Vec_PtrFree( p->vCutsNew );
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index bbceac47..402b7cdd 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -368,10 +368,9 @@ struct FxuSingle // 7 words
 // iterator through the cube pairs belonging to the given cube 
 #define Fxu_CubeForEachPair( pCube, pPair, i )\
   for ( i = 0;\
-        i < pCube->pVar->nCubes &&\
-        (((unsigned)(ABC_PTRUINT_T)(pPair = pCube->pVar->ppPairs[pCube->iCube][i])) >= 0);\
+        i < pCube->pVar->nCubes && (((pPair) = (pCube)->pVar->ppPairs[(pCube)->iCube][i]), 1);\
         i++ )\
-        if ( pPair )
+        if ( pPair == NULL ) {} else
 
 // iterator through all the items in the heap
 #define Fxu_HeapDoubleForEachItem( Heap, Div )\
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 2321ec57..b0e3e4a7 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -67,7 +67,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     assert( nPairsMax < nPairsTotal );
 
     // allocate storage for counter of diffs
-    pnLitsDiff = ABC_ALLOC( unsigned char, nPairsTotal );
+    pnLitsDiff = ABC_FALLOC( unsigned char, nPairsTotal );
     // go through the covers and precompute the distances between the pairs
     iPair    =  0;
     nBitsMax = -1;
@@ -86,7 +86,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     assert( iPair == nPairsTotal );
 
     // allocate storage for counters of cube pairs by difference
-    pnPairCounters = ABC_ALLOC( int, 2 * nBitsMax );
+    pnPairCounters = ABC_FALLOC( int, 2 * nBitsMax );
     memset( pnPairCounters, 0, sizeof(int) * 2 * nBitsMax );
     // count the number of different pairs
     for ( k = 0; k < nPairsTotal; k++ )
@@ -95,11 +95,15 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
     // so that there would be exactly pPairsMax pairs
     if ( pnPairCounters[0] != 0 )
     {
+        ABC_FREE( pnLitsDiff );
+        ABC_FREE( pnPairCounters );
         printf( "The SOPs of the nodes are not cube-ABC_FREE. Run \"bdd; sop\" before \"fx\".\n" );
         return 0;
     }
     if ( pnPairCounters[1] != 0 )
     {
+        ABC_FREE( pnLitsDiff );
+        ABC_FREE( pnPairCounters );
         printf( "The SOPs of the nodes are not SCC-ABC_FREE. Run \"bdd; sop\" before \"fx\".\n" );
         return 0;
     }
diff --git a/src/opt/fxu/fxuSelect.c b/src/opt/fxu/fxuSelect.c
index a4e260c7..c9945926 100644
--- a/src/opt/fxu/fxuSelect.c
+++ b/src/opt/fxu/fxuSelect.c
@@ -57,12 +57,12 @@ void Fxu_MatrixGetDoubleVars( Fxu_Matrix * p, Fxu_Double * pDouble,
 int Fxu_Select( Fxu_Matrix * p, Fxu_Single ** ppSingle, Fxu_Double ** ppDouble )
 {
     // the top entries
-    Fxu_Single * pSingles[MAX_SIZE_LOOKAHEAD];
-    Fxu_Double * pDoubles[MAX_SIZE_LOOKAHEAD];
+    Fxu_Single * pSingles[MAX_SIZE_LOOKAHEAD] = {0};
+    Fxu_Double * pDoubles[MAX_SIZE_LOOKAHEAD] = {0};
     // the complements
-    Fxu_Double * pSCompl[MAX_SIZE_LOOKAHEAD];
-    Fxu_Single * pDComplS[MAX_SIZE_LOOKAHEAD];
-    Fxu_Double * pDComplD[MAX_SIZE_LOOKAHEAD];
+    Fxu_Double * pSCompl[MAX_SIZE_LOOKAHEAD] = {0};
+    Fxu_Single * pDComplS[MAX_SIZE_LOOKAHEAD] = {0};
+    Fxu_Double * pDComplD[MAX_SIZE_LOOKAHEAD] = {0};
     Fxu_Pair * pPair;
     int nSingles;
     int nDoubles;
diff --git a/src/opt/ret/retLvalue.c b/src/opt/ret/retLvalue.c
index 7d32dd7d..95569867 100644
--- a/src/opt/ret/retLvalue.c
+++ b/src/opt/ret/retLvalue.c
@@ -104,6 +104,7 @@ Vec_Int_t * Abc_NtkRetimeGetLags( Abc_Ntk_t * pNtk, int nIterLimit, int fVerbose
     vLatches = Abc_ManCollectLatches( pNtk );
     if ( !Abc_NtkRetimeForPeriod( pNtk, vNodes, vLatches, FiMax, nIterLimit, fVerbose ) )
     {
+        Vec_PtrFree( vLatches );
         Vec_PtrFree( vNodes );
         printf( "Abc_NtkRetimeGetLags() error: The upper bound on the clock period cannot be computed.\n" );
         return Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );