Version abc80702

author: Alan Mishchenko <alanmi@berkeley.edu> 2008-07-02 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2008-07-02 08:01:00 -0700
commit: 303baf27cf34c2a57db97c4c567fd744241fa14b (patch)
tree: d6235cca48e7bdfe5884e517058c7791e66bb806 /src/base
parent: fa67e3c19e27c011517b91182eb3929412aaf402 (diff)
download: abc-303baf27cf34c2a57db97c4c567fd744241fa14b.tar.gz
abc-303baf27cf34c2a57db97c4c567fd744241fa14b.tar.bz2
abc-303baf27cf34c2a57db97c4c567fd744241fa14b.zip
66 files changed, 598 insertions, 354 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 8f0c7210..9cb7a855 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -439,10 +439,10 @@ static inline bool        Abc_LatchIsInitNone( Abc_Obj_t * pLatch )  { assert(Ab
 static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
 static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;  }
 static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;   }
-static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData;                     }
+static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Abc_ObjIsLatch(pLatch)); return (int)(PORT_PTRINT_T)pLatch->pData;      }
 
 // global BDDs of the nodes
-static inline void *      Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk )          { return (void *)Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD);             }
+static inline void *      Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk )          { return (void *)Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD);                          }
 static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return (DdManager *)Vec_AttMan( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
 static inline DdNode **   Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return (DdNode **)Vec_AttArray( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
 static inline DdNode *    Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return (DdNode *)Vec_AttEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );    }
diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c
index f945696e..3d6730e7 100644
--- a/src/base/abc/abcBlifMv.c
+++ b/src/base/abc/abcBlifMv.c
@@ -43,7 +43,7 @@ void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk )
 {
     Vec_Att_t * pAttMan;
     assert( Abc_NtkMvVar(pNtk) == NULL );
-    pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), Extra_MmFlexStop, NULL, NULL );
+    pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), (void(*)(void*))Extra_MmFlexStop, NULL, NULL );
     Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan );
 //printf( "allocing attr\n" );
 }
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index a78632d2..e538bd64 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -234,7 +234,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pObj;
+    Abc_Obj_t * pObj = NULL; // Ensure pObj isn't used uninitialized.
     Vec_Int_t * vNameIds;
     char * pName;
     int i, NameId;
@@ -262,6 +262,8 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
         }
     }
 
+    assert(pObj); // pObj should point to something here.
+
     // return the array of all IDs, which have names
     vNameIds = Nm_ManReturnNameIds( pNtk->pManName );
     // make sure that these IDs correspond to live objects
@@ -571,10 +573,10 @@ bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
         Value = 0;
     }
     // make sure the latch has a reasonable return value
-    if ( (int)pLatch->pData < ABC_INIT_ZERO || (int)pLatch->pData > ABC_INIT_DC )
+    if ( (int)(PORT_PTRINT_T)pLatch->pData < ABC_INIT_ZERO || (int)(PORT_PTRINT_T)pLatch->pData > ABC_INIT_DC )
     {
         fprintf( stdout, "NodeCheck: Latch \"%s\" has incorrect reset value (%d).\n", 
-            Abc_ObjName(pLatch), (int)pLatch->pData );
+            Abc_ObjName(pLatch), (int)(PORT_PTRINT_T)pLatch->pData );
         Value = 0;
     }
     // make sure the latch has only one fanin
@@ -857,7 +859,7 @@ int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk )
     for ( i = 1; i < Abc_NtkCiNum(pNtk); i++ )
         if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) )
         {
-            printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) );
+            printf( "Abc_NtkCheck: Repeated CI names: %s and %s.\n", (char*)Vec_PtrEntry(vNames,i-1), (char*)Vec_PtrEntry(vNames,i) );
             fRetValue = 0;
         }
     Vec_PtrFree( vNames );
@@ -890,7 +892,7 @@ int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk )
 //        printf( "%s\n", Vec_PtrEntry(vNames,i) );
         if ( !strcmp( Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) ) )
         {
-            printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", Vec_PtrEntry(vNames,i-1), Vec_PtrEntry(vNames,i) );
+            printf( "Abc_NtkCheck: Repeated CO names: %s and %s.\n", (char*)Vec_PtrEntry(vNames,i-1), (char*)Vec_PtrEntry(vNames,i) );
             fRetValue = 0;
         }
     }
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index b5fb81db..8759500b 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -197,10 +197,11 @@ Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
             Abc_NtkDfsReverse_rec( pFanout, vNodes );
     }
     // add constant nodes in the end
-    if ( !Abc_NtkIsStrash(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) ) {
         Abc_NtkForEachNode( pNtk, pObj, i )
             if ( Abc_NodeIsConst(pObj) )
                 Vec_PtrPush( vNodes, pObj );
+    }
     return vNodes;
 }
 
@@ -492,7 +493,7 @@ void Abc_NtkDfs_iter( Vec_Ptr_t * vStack, Abc_Obj_t * pRoot, Vec_Ptr_t * vNodes
     while ( Vec_PtrSize(vStack) > 0 )
     {
         // get the node and its fanin
-        iFanin = (int)Vec_PtrPop(vStack);
+        iFanin = (int)(PORT_PTRINT_T)Vec_PtrPop(vStack);
         pNode  = Vec_PtrPop(vStack);
         assert( !Abc_ObjIsNet(pNode) );
         // add it to the array of nodes if we finished
@@ -503,7 +504,7 @@ void Abc_NtkDfs_iter( Vec_Ptr_t * vStack, Abc_Obj_t * pRoot, Vec_Ptr_t * vNodes
         }
         // explore the next fanin
         Vec_PtrPush( vStack, pNode );
-        Vec_PtrPush( vStack, (void *)(iFanin+1) );
+        Vec_PtrPush( vStack, (void *)(PORT_PTRINT_T)(iFanin+1) );
         // get the fanin
         pFanin = Abc_ObjFanin0Ntk( Abc_ObjFanin(pNode,iFanin) );
         // if this node is already visited, skip
@@ -1112,7 +1113,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     Abc_NodeSetTravIdCurrent( pNode );
     // visit the transitive fanin
     Abc_ObjForEachFanin( pNode, pFanin, i )
-    {
+    { 
         pFanin = Abc_ObjFanin0Ntk(pFanin);
         // make sure there is no mixing of networks
         assert( pFanin->pNtk == pNode->pNtk );
@@ -1120,7 +1121,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
         if ( Abc_NodeIsTravIdPrevious(pFanin) ) 
             continue;
         // traverse the fanin's cone searching for the loop
-        if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
+        if ( (fAcyclic = Abc_NtkIsAcyclic_rec(pFanin)) )
             continue;
         // return as soon as the loop is detected
         fprintf( stdout, " %s ->", Abc_ObjName(pFanin) );
@@ -1135,7 +1136,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
             if ( Abc_NodeIsTravIdPrevious(pFanin) ) 
                 continue;
             // traverse the fanin's cone searching for the loop
-            if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
+            if ( (fAcyclic = Abc_NtkIsAcyclic_rec(pFanin)) )
                 continue;
             // return as soon as the loop is detected
             fprintf( stdout, " %s", Abc_ObjName(pFanin) );
@@ -1184,7 +1185,7 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
         if ( Abc_NodeIsTravIdPrevious(pNode) )
             continue;
         // traverse the output logic cone
-        if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) )
+        if ( (fAcyclic = Abc_NtkIsAcyclic_rec(pNode)) )
             continue;
         // stop as soon as the first loop is detected
         fprintf( stdout, " CO \"%s\"\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
@@ -1211,7 +1212,7 @@ int Abc_NodeSetChoiceLevel_rec( Abc_Obj_t * pNode, int fMaximum )
     int Level1, Level2, Level, LevelE;
     // skip the visited node
     if ( Abc_NodeIsTravIdCurrent( pNode ) )
-        return (int)pNode->pCopy;
+        return (int)(PORT_PTRINT_T)pNode->pCopy;
     Abc_NodeSetTravIdCurrent( pNode );
     // compute levels of the children nodes
     Level1 = Abc_NodeSetChoiceLevel_rec( Abc_ObjFanin0(pNode), fMaximum );
@@ -1226,9 +1227,9 @@ int Abc_NodeSetChoiceLevel_rec( Abc_Obj_t * pNode, int fMaximum )
             Level = ABC_MIN( Level, LevelE );
         // set the level of all equivalent nodes to be the same minimum
         for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
-            pTemp->pCopy = (void *)Level;
+            pTemp->pCopy = (void *)(PORT_PTRINT_T)Level;
     }
-    pNode->pCopy = (void *)Level;
+    pNode->pCopy = (void *)(PORT_PTRINT_T)Level;
     return Level;
 }
 
@@ -1297,7 +1298,7 @@ Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis )
     vLevels = Vec_PtrStart( LevelMax + 1 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        ppHead = ((Abc_Obj_t **)vLevels->pArray) + (int)pNode->pCopy;
+        ppHead = ((Abc_Obj_t **)vLevels->pArray) + (int)(PORT_PTRINT_T)pNode->pCopy;
         pNode->pCopy = *ppHead;
         *ppHead = pNode;
     }
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 9f60b0bc..14b2b0c1 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -90,14 +90,8 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
     if ( Abc_ObjIsNet(pObj) && Abc_ObjFaninNum(pObj) > 1 )
     {
-        int x = 0; 
+        printf( "Abc_ObjAddFanin(): Error! Creating net with two fanins.\n" );
     }
-    if ( pObj->Id == 1960 )
-    {
-        int x = 0;
-    }
-//    printf( "Adding fanin of %s ", Abc_ObjName(pObj) );
-//    printf( "to be %s\n", Abc_ObjName(pFanin) );
 }
 
 
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 4529d9f3..79b60cf9 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -208,7 +208,7 @@ void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues )
     Abc_Obj_t * pLatch;
     int i;
     Abc_NtkForEachLatch( pNtk, pLatch, i )
-        pLatch->pData = (void *)(vValues? (Vec_IntEntry(vValues,i)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
+        pLatch->pData = (void *)(PORT_PTRINT_T)(vValues? (Vec_IntEntry(vValues,i)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
 }
 
 /**Function*************************************************************
@@ -340,7 +340,7 @@ Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk )
         return NULL;
     // set register numbers
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pNext = (Abc_Obj_t *)i;
+        pObj->pNext = (Abc_Obj_t *)(PORT_PTRINT_T)i;
     // add the numbers
     vResult = Vec_PtrAlloc( Vec_PtrSize(pNtk->vOnehots) );
     Vec_PtrForEachEntry( pNtk->vOnehots, vNames, i )
@@ -354,7 +354,7 @@ Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk )
             pObj = Abc_NtkObj( pNtk, Num );
             if ( Abc_ObjFaninNum(pObj) != 1 || !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) )
                 continue;
-            Vec_IntPush( vNumbers, (int)pObj->pNext );
+            Vec_IntPush( vNumbers, (int)(PORT_PTRINT_T)pObj->pNext );
         }
         if ( Vec_IntSize( vNumbers ) > 1 )
         {
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 4d543547..88bcda69 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -932,7 +932,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     void * pAttrMan;
     int TotalMemory, i;
-    int LargePiece = (4 << ABC_NUM_STEPS);
+//    int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
     // free the HAIG
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 79bf41a1..a79eb5a7 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -70,7 +70,7 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
 void Abc_ObjRecycle( Abc_Obj_t * pObj )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    int LargePiece = (4 << ABC_NUM_STEPS);
+//    int LargePiece = (4 << ABC_NUM_STEPS);
     // free large fanout arrays
 //    if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
 //        FREE( pObj->vFanouts.pArray );
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 3bac7316..2b406e81 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -20,8 +20,11 @@
 
 #ifdef WIN32
 #include <process.h> 
+#else
+#include <unistd.h>
 #endif
 
+
 #include "abc.h"
 #include "main.h"
 #include "ioAbc.h"
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index b2d6b649..d1d1a468 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -804,7 +804,7 @@ bool Abc_SopCheck( char * pSop, int nFanins )
         if ( pCubes - pCubesOld != nFanins )
         {
             fprintf( stdout, "Abc_SopCheck: SOP has a mismatch between its cover size (%d) and its fanin number (%d).\n",
-                pCubes - pCubesOld, nFanins );
+                (int)(PORT_PTRDIFF_T)(pCubes - pCubesOld), nFanins );
             return 0;
         }
         // check the output values for this cube
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index d3d32b98..39f44c11 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1536,9 +1536,9 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk )
 static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj )
 {
 //    pObj->pCopy = (void *)(((int)pObj->pCopy)++);
-    int Value = (int)pObj->pCopy;
-    pObj->pCopy = (void *)(Value + 1);
-    return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj);
+    int Value = (int)(PORT_PTRINT_T)pObj->pCopy;
+    pObj->pCopy = (void *)(PORT_PTRINT_T)(Value + 1);
+    return (int)(PORT_PTRINT_T)pObj->pCopy == Abc_ObjFanoutNum(pObj);
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d3372c9a..ae1c110f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -506,7 +506,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
         Dar_LibStart();
     }
     {
-        extern Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
+        extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
 //        Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 );
     }
 
@@ -3710,7 +3710,6 @@ int Abc_CommandTrace( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    Mfs_Par_t Pars, * pPars = &Pars;
     int c;
     int fUseLutLib;
     int fVerbose;
@@ -3780,7 +3779,6 @@ int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    Mfs_Par_t Pars, * pPars = &Pars;
     int c;
     int fUseLutLib;
     int Percentage;
@@ -6568,7 +6566,7 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" )) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -6655,7 +6653,7 @@ int Abc_CommandCareSet( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" )) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -6706,7 +6704,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cut_Params_t Params, * pParams = &Params;
     Cut_Man_t * pCutMan;
-    Cut_Oracle_t * pCutOracle;
+    Cut_Oracle_t * pCutOracle = NULL;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
@@ -6829,6 +6827,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cut_ManStop( pCutMan );
     if ( fOracle )
     {
+        assert(pCutOracle);
         Abc_NtkCutsOracle( pNtk, pCutOracle );
         Cut_OracleStop( pCutOracle );
     }
@@ -15673,7 +15672,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( pFileName, "r" )) == NULL )
     {
         fprintf( stdout, "Cannot open input file \"%s\". ", pFileName );
-        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL ) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL )) )
             fprintf( stdout, "Did you mean \"%s\"?", pFileName );
         fprintf( stdout, "\n" );
         return 1;
@@ -15763,7 +15762,7 @@ int Abc_CommandAbc8ReadLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( pFileName, "r" )) == NULL )
     {
         fprintf( stdout, "Cannot open input file \"%s\". ", pFileName );
-        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL ) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL )) )
             fprintf( stdout, "Did you mean \"%s\"?", pFileName );
         fprintf( stdout, "\n" );
         return 1;
@@ -16032,7 +16031,7 @@ int Abc_CommandAbc8ReadLut( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( stdout, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL ) )
+        if ( (FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL )) )
             fprintf( stdout, "Did you mean \"%s\"?", FileName );
         fprintf( stdout, "\n" );
         return 1;
@@ -17041,11 +17040,11 @@ int Abc_CommandAbc8Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Aig_Man_t * pAigNew;
     int c;
-    int fUseLutLib;
-    int Percentage;
-    int Degree;
-    int fVerbose;
-    int fVeryVerbose;
+    int fUseLutLib = 0;
+    int Percentage = 100;
+    int Degree = 5;
+    int fVerbose = 0;
+    int fVeryVerbose = 0;
     extern Aig_Man_t * Nwk_ManSpeedup( void * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
 
     // set defaults
diff --git a/src/base/abci/abcAbc8.c b/src/base/abci/abcAbc8.c
index d58f6b7e..be25d9c2 100644
--- a/src/base/abci/abcAbc8.c
+++ b/src/base/abci/abcAbc8.c
@@ -253,7 +253,6 @@ Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib )
     extern Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
     extern Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
 
-    Mfx_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkNew;
     Nwk_Man_t * pMan;
     pMan = Abc_NtkToNtkNew( pNtk );
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index f04837c5..26b6db99 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -96,7 +96,6 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective,
 ***********************************************************************/
 void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective, bool fUpdateLevel )
 {
-    int fCheck = 1;
     ProgressBar * pProgress;
     Vec_Vec_t * vStorage;
     Abc_Obj_t * pNode, * pDriver;
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
index af6d237b..1512c76f 100644
--- a/src/base/abci/abcBmc.c
+++ b/src/base/abci/abcBmc.c
@@ -84,7 +84,7 @@ printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
 ***********************************************************************/
 void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames )
 {
-    Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3;
+    Ivy_Obj_t * pFirst1, * pFirst2 = NULL, * pFirst3 = NULL;
     int i, f, nIdMax, Prev2, Prev3;
     nIdMax = Ivy_ManObjIdMax(pMan);
     // check what is the number of nodes in each frame
@@ -101,6 +101,8 @@ void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig
                 continue;
             break;
         }
+        assert(pFirst2);
+        assert(pFirst3);
         if ( f )
             printf( "Frame %3d :  Strash = %5d  Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 );
         Prev2 = pFirst2->Id;
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index d399ce5f..d38f62d0 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -144,7 +144,7 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
 {
     Abc_Obj_t * pObj;
     Vec_Ptr_t * vNodes;
-    int i, clk = clock();
+    int i; //, clk = clock();
     int fDrop = Cut_OracleReadDrop(p);
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -327,7 +327,7 @@ int Abc_NtkComputeArea( Abc_Ntk_t * pNtk, Cut_Man_t * p )
 void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
     void * pList;
-    if ( pList = Abc_NodeReadCuts( p, pObj ) )
+    if ( (pList = Abc_NodeReadCuts( p, pObj )) )
         return pList;
     Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree );
     Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree );
@@ -459,7 +459,6 @@ void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
 ***********************************************************************/
 void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq )
 {
-    Cut_Man_t * pMan = p;
     Cut_Cut_t * pList;
     Abc_Obj_t * pObj;
     int i;
@@ -485,7 +484,6 @@ void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq )
 ***********************************************************************/
 void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
 {
-    Cut_Man_t * pMan = p;
     Cut_Cut_t * pList;
     Abc_Obj_t * pObj;
     pObj = Abc_NtkObj( pNtk, 2 * Abc_NtkObjNum(pNtk) / 3 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d746e315..d89ee618 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -99,10 +99,11 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
     // complement the 1-values registers
-    if ( fRegisters )
+    if ( fRegisters ) {
         Abc_NtkForEachLatch( pNtk, pObj, i )
             if ( Abc_LatchIsInit1(pObj) )
                 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
+    }
     // perform the conversion of the internal nodes (assumes DFS ordering)
 //    pMan->fAddStrash = 1;
     Abc_NtkForEachNode( pNtk, pObj, i )
@@ -1894,7 +1895,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation
 {
     Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
     Abc_Obj_t * pObj;
-    int i, clk = clock();
+    int i; //, clk = clock();
     if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
     {
         printf( "Currently works only for networks with equal number of POs.\n" );
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index 3c28e6a6..91f175fa 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -526,8 +526,8 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
         printf( "\n" );
     }
     // mark the timing critical nodes and edges
-    puTCEdges = ALLOC( int, Abc_NtkObjNumMax(pNtk) );
-    memset( puTCEdges, 0, sizeof(int) * Abc_NtkObjNumMax(pNtk) );
+    puTCEdges = ALLOC( unsigned, Abc_NtkObjNumMax(pNtk) );
+    memset( puTCEdges, 0, sizeof(unsigned) * Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         if ( Abc_ObjSlack(pNode) >= tDelta )
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index c00a7d7c..ab6279b6 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -161,11 +161,11 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     int i, nNodesDsd;
 
     // save the CI nodes in the DSD nodes
-    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) );
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(PORT_PTRINT_T)Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
-        Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy );
+        Dsd_NodeSetMark( pNodeDsd, (int)(PORT_PTRINT_T)pNode->pCopy );
     }
 
     // collect DSD nodes in DFS order (leaves and const1 are not collected)
@@ -183,7 +183,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
         if ( !Abc_AigNodeIsAnd(pDriver) )
             continue;
         pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
-        pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
+        pNodeNew = (Abc_Obj_t *)(PORT_PTRINT_T)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
         assert( !Abc_ObjIsComplement(pNodeNew) );
         pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
     }
@@ -219,7 +219,7 @@ Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNode
     for ( i = 0; i < nDecs; i++ )
     {
         pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
-        pFanin     = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
+        pFanin     = (Abc_Obj_t *)(PORT_PTRINT_T)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
         Abc_ObjAddFanin( pNodeNew, pFanin );
         assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
     }
@@ -284,7 +284,7 @@ printf( "\n" );
         }
     }
     pNodeNew->pData = bLocal;
-    Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew );
+    Dsd_NodeSetMark( pNodeDsd, (int)(PORT_PTRINT_T)pNodeNew );
     return pNodeNew;
 }
 
@@ -383,7 +383,7 @@ Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk )
 void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd, bool fRecursive, int * pCounters )
 {
     DdManager * dd = pNode->pNtk->pManFunc;
-    Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
+    Abc_Obj_t * pRoot = NULL, * pFanin, * pNode1, * pNode2, * pNodeC;
     Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd;
     int i, nNodesDsd, iVar, fCompl;
 
@@ -400,7 +400,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
         Abc_ObjForEachFanin( pNode, pFanin, i )
         {
             pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
-            Dsd_NodeSetMark( pFaninDsd, (int)pFanin );
+            Dsd_NodeSetMark( pFaninDsd, (int)(PORT_PTRINT_T)pFanin );
         }
 
         // construct the intermediate nodes
@@ -412,6 +412,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
                 Vec_PtrPush( vNodes, pRoot );
         }
         free( ppNodesDsd );
+        assert(pRoot);
 
         // remove the current fanins
         Abc_ObjRemoveFanins( pNode );
@@ -466,7 +467,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
 ***********************************************************************/
 bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
 {
-    DdManager * dd = pNode->pNtk->pManFunc;
+//    DdManager * dd = pNode->pNtk->pManFunc;
 //    DdNode * bFunc, * bFunc0, * bFunc1;
     assert( Abc_ObjIsNode(pNode) );
 //    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 78e7cf6b..b87edb6b 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -49,7 +49,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int
     int fShowSwitching = 1;
     Abc_Ntk_t * pNtkNew;
     Fpga_Man_t * pMan;
-    Vec_Int_t * vSwitching;
+    Vec_Int_t * vSwitching = NULL;
     float * pSwitching = NULL;
     int Num;
 
@@ -70,7 +70,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int
 
     // perform FPGA mapping
     pMan = Abc_NtkToFpga( pNtk, fRecovery, pSwitching, fLatchPaths, fVerbose );    
-    if ( pSwitching ) Vec_IntFree( vSwitching );
+    if ( pSwitching ) { assert(vSwitching); Vec_IntFree( vSwitching ); }
     if ( pMan == NULL )
         return NULL;
     Fpga_ManSetSwitching( pMan, fSwitching );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index be8a25f1..d3cbaccb 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -101,7 +101,7 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExd
 {
     int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
     Fraig_Man_t * pMan;
-    ProgressBar * pProgress;
+    ProgressBar * pProgress = NULL;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i;
@@ -126,14 +126,18 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExd
     {
         if ( Abc_ObjFaninNum(pNode) == 0 )
             continue;
-        if ( !fInternal )
+        if ( !fInternal ) {
+            assert(pProgress);
             Extra_ProgressBarUpdate( pProgress, i, NULL );
+        }
         pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
                 Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
     }
-    if ( !fInternal )
+    if ( !fInternal ) {
+        assert(pProgress);
         Extra_ProgressBarStop( pProgress );
+    }
     Vec_PtrFree( vNodes );
 
     // use EXDC to change the mapping of nodes into FRAIG nodes
@@ -316,7 +320,7 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai
     Fraig_Node_t * pNodeTemp, * pNodeFraigR = Fraig_Regular(pNodeFraig);
     void ** ppTail;
     // check if the node was already considered
-    if ( pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR) )
+    if ( (pRes = (Abc_Obj_t *)Fraig_NodeReadData1(pNodeFraigR)) )
         return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
     // solve the children
     pRes0 = Abc_NodeFromFraig_rec( pNtkNew, Fraig_NodeReadOne(pNodeFraigR) );
@@ -455,7 +459,7 @@ void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t *
     Abc_NodeSetTravIdCurrent( pNode );
     assert( Abc_ObjIsNode( pNode ) );
     // get the node's representative
-    if ( pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id) )
+    if ( (pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id)) )
     {
         Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
         pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
@@ -695,7 +699,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Vec_Ptr_t * vStore;
     Abc_Ntk_t * pNtk, * pFraig;
     int nWords1, nWords2, nWordsMin;
-    int clk = clock();
+//    int clk = clock();
 
     // get the stored network
     vStore = Abc_FrameReadStore();
@@ -732,6 +736,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Params.fDoSparse  =    1;              // performs equiv tests for sparse functions 
     Params.fChoicing  =    1;              // enables recording structural choices
     Params.fTryProve  =    0;              // tries to solve the final miter
+    Params.fInternal  =    1;              // does not show progress bar
     Params.fVerbose   =    0;              // the verbosiness flag
 
     // perform partitioned computation of structural choices
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 94c7dda8..751e2b2f 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -453,8 +453,8 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
 ***********************************************************************/
 int Abc_ObjCompareFlow( Abc_Obj_t ** ppNode0, Abc_Obj_t ** ppNode1 )
 {
-    float Flow0 = Abc_Int2Float((int)(*ppNode0)->pCopy);
-    float Flow1 = Abc_Int2Float((int)(*ppNode1)->pCopy);
+    float Flow0 = Abc_Int2Float((int)(PORT_PTRINT_T)(*ppNode0)->pCopy);
+    float Flow1 = Abc_Int2Float((int)(PORT_PTRINT_T)(*ppNode1)->pCopy);
     if ( Flow0 > Flow1 )
         return -1;
     if ( Flow0 < Flow1 )
@@ -517,9 +517,9 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
     {
         pFanin0 = Abc_ObjFanin0(pNode);
         pFanin1 = Abc_ObjFanin1(pNode);
-        Flow0 = Abc_Int2Float((int)pFanin0->pCopy)/Abc_ObjFanoutNum(pFanin0);
-        Flow1 = Abc_Int2Float((int)pFanin1->pCopy)/Abc_ObjFanoutNum(pFanin1);
-        pNode->pCopy = (Abc_Obj_t *)Abc_Float2Int(Flow0 + Flow1+(float)1.0);
+        Flow0 = Abc_Int2Float((int)(PORT_PTRINT_T)pFanin0->pCopy)/Abc_ObjFanoutNum(pFanin0);
+        Flow1 = Abc_Int2Float((int)(PORT_PTRINT_T)pFanin1->pCopy)/Abc_ObjFanoutNum(pFanin1);
+        pNode->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)Abc_Float2Int(Flow0 + Flow1+(float)1.0);
     }
     // find the flow of the COs
     vCos = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
@@ -536,7 +536,7 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
     // verify sorting
     pFanin0 = Vec_PtrEntry(vCos, 0);
     pFanin1 = Vec_PtrEntryLast(vCos);
-    assert( Abc_Int2Float((int)pFanin0->pCopy) >= Abc_Int2Float((int)pFanin1->pCopy) );
+    assert( Abc_Int2Float((int)(PORT_PTRINT_T)pFanin0->pCopy) >= Abc_Int2Float((int)(PORT_PTRINT_T)pFanin1->pCopy) );
 
     // collect the nodes in the topological order from the new array
     Abc_NtkIncrementTravId( pNtk );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index a470448e..96d8196e 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -73,7 +73,6 @@ extern int timeRetime;
 Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
 {
     Ivy_Man_t * pMan;
-    int fCleanup = 1;
 //timeRetime = clock();
     assert( !Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
@@ -588,9 +587,9 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 {
 //    Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;//, * pTemp;
-    int fCleanup = 1;
+//    int fCleanup = 1;
 //    int nNodes;
-    int nLatches = Abc_NtkLatchNum(pNtk);
+//    int nLatches = Abc_NtkLatchNum(pNtk);
     Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
 
     assert( !Abc_NtkIsNetlist(pNtk) );
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index afa76cc8..4203a425 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -21,6 +21,8 @@
 #include "abc.h"
 #include "cut.h"
 
+#define LARGE_LEVEL 1000000
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -212,7 +214,7 @@ void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj )
     assert( pCut != NULL );
     assert( pObj->Level == 0 );
     // go through the cuts
-    pObj->Level = ABC_INFINITY;
+    pObj->Level = LARGE_LEVEL;
     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
     {
         DelayMax = 0;
@@ -226,7 +228,7 @@ void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj )
         if ( (int)pObj->Level > DelayMax )
             pObj->Level = DelayMax;
     }
-    assert( pObj->Level < ABC_INFINITY );
+    assert( pObj->Level < LARGE_LEVEL );
     pObj->Level++;
 //    printf( "%d(%d) ", pObj->Id, pObj->Level );
 }
@@ -340,7 +342,7 @@ void Abc_ManSclStop( Abc_ManScl_t * p )
 unsigned * Abc_NodeSuperChoiceTruth( Abc_ManScl_t * pManScl )
 {
     Abc_Obj_t * pObj;
-    unsigned * puData0, * puData1, * puData;
+    unsigned * puData0, * puData1, * puData = NULL;
     char * pSop;
     int i, k;
     // set elementary truth tables
@@ -635,7 +637,7 @@ void Abc_NodeDecomposeSort( Abc_Obj_t ** pLeaves, int nVars, int * pBSet, int nL
     for ( i = 0; i < nLutSize; i++ )
     {
         kBest = -1;
-        LevelMin = ABC_INFINITY;
+        LevelMin = LARGE_LEVEL;
         for ( k = 0; k < nVars; k++ )
             if ( pTemp[k] && LevelMin > (int)pTemp[k]->Level )
             {
@@ -704,7 +706,7 @@ int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
             pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
             if ( Extra_TruthIsEqual( pTruthCof, pTruthClass, nVars ) )
             {
-                pCofClasses[k][ nCofClasses[k]++ ] = i;
+                pCofClasses[k][(int)nCofClasses[k]++ ] = i;
                 break;
             }
         }
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index d4d50923..f6a1bb4e 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -59,7 +59,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     int fShowSwitching = 1;
     Abc_Ntk_t * pNtkNew;
     Map_Man_t * pMan;
-    Vec_Int_t * vSwitching;
+    Vec_Int_t * vSwitching = NULL;
     float * pSwitching = NULL;
     int clk;
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 3de3eefa..ed02f589 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -258,7 +258,7 @@ DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDrop
     // start the manager
     assert( Abc_NtkGlobalBdd(pNtk) == NULL );
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, dd, Extra_StopManager, NULL, Cudd_RecursiveDeref );
+    pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, dd, (void (*)(void*))Extra_StopManager, NULL, (void (*)(void*,void*))Cudd_RecursiveDeref );
     Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
 
     // set reordering
diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
index d6e59328..989d551f 100644
--- a/src/base/abci/abcOdc.c
+++ b/src/base/abci/abcOdc.c
@@ -662,10 +662,10 @@ void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t
     assert( Abc_ObjIsNode(pNode) );
     // consider the case when the node is the pivot
     if ( pNode == pPivot )
-        return pNode->pCopy = (void *)((Odc_Const1() << 16) | Odc_Const0());
+        return pNode->pCopy = (void *)(PORT_PTRUINT_T)((Odc_Const1() << 16) | Odc_Const0());
     // compute the cofactors
-    uData0 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
-    uData1 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
+    uData0 = (unsigned)(PORT_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
+    uData1 = (unsigned)(PORT_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
     // find the 0-cofactor
     uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
@@ -675,7 +675,7 @@ void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t
     uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
     uRes1 = Odc_And( p, uLit0, uLit1 );
     // find the result
-    return pNode->pCopy = (void *)((uRes1 << 16) | uRes0);
+    return pNode->pCopy = (void *)(PORT_PTRUINT_T)((uRes1 << 16) | uRes0);
 }
 
 /**Function*************************************************************
@@ -701,21 +701,21 @@ int Abc_NtkDontCareTransfer( Odc_Man_t * p )
     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
     {
         uLit = Odc_Var( p, i );
-        pObj->pCopy = (void *)((uLit << 16) | uLit);
+        pObj->pCopy = (void *)(PORT_PTRUINT_T)((uLit << 16) | uLit);
         Abc_NodeSetTravIdCurrent(pObj);
     }
     // set elementary variables at the branched 
     Vec_PtrForEachEntry( p->vBranches, pObj, i )
     {
         uLit = Odc_Var( p, i+p->nVarsMax );
-        pObj->pCopy = (void *)((uLit << 16) | uLit);
+        pObj->pCopy = (void *)(PORT_PTRUINT_T)((uLit << 16) | uLit);
         Abc_NodeSetTravIdCurrent(pObj);
     }
     // compute the AIG for the window
     p->iRoot = Odc_Const0();
     Vec_PtrForEachEntry( p->vRoots, pObj, i )
     {
-        uData = (unsigned)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
+        uData = (unsigned)(PORT_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
         // get the cofactors
         uRes0 = uData & 0xffff;
         uRes1 = uData >> 16;
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 85c4e918..a482e5c9 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -115,7 +115,7 @@ char * Supp_ManFetch( Supp_Man_t * p, int nSize )
     assert( nSize > 0 );
     Type = Supp_SizeType( nSize, p->nStepSize );
     Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
-    if ( pMemory = Vec_PtrEntry( p->vFree, Type ) )
+    if ( (pMemory = Vec_PtrEntry( p->vFree, Type )) )
     {
         Vec_PtrWriteEntry( p->vFree, Type, Supp_OneNext(pMemory) );
         return pMemory;
@@ -321,9 +321,9 @@ Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
     int i;
     // set the number of PIs/POs
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pNext = (Abc_Obj_t *)i;
+        pObj->pNext = (Abc_Obj_t *)(PORT_PTRINT_T)i;
     Abc_NtkForEachCo( pNtk, pObj, i )
-        pObj->pNext = (Abc_Obj_t *)i;
+        pObj->pNext = (Abc_Obj_t *)(PORT_PTRINT_T)i;
     // start the support computation manager
     p = Supp_ManStart( 1 << 20, 1 << 6 );
     // consider objects in the topological order
@@ -353,7 +353,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
             if ( Abc_ObjIsNode(Abc_ObjFanin0(pObj)) )
             {
                 vSupp = Supp_ManTransferEntry(pPart0);
-                Vec_IntPush( vSupp, (int)pObj->pNext );
+                Vec_IntPush( vSupp, (int)(PORT_PTRINT_T)pObj->pNext );
                 Vec_PtrPush( vSupports, vSupp );
             }
             assert( pPart0->nRefs > 0 );
@@ -366,7 +366,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsSmart( Abc_Ntk_t * pNtk )
             if ( Abc_ObjFanoutNum(pObj) )
             {
                 pPart0 = (Supp_One_t *)Supp_ManFetchEntry( p, 1, Abc_ObjFanoutNum(pObj) );
-                pPart0->pOuts[ pPart0->nOuts++ ] = (int)pObj->pNext;
+                pPart0->pOuts[ pPart0->nOuts++ ] = (int)(PORT_PTRINT_T)pObj->pNext;
                 pObj->pCopy = (Abc_Obj_t *)pPart0;
             }
             continue;
@@ -417,7 +417,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsNaive( Abc_Ntk_t * pNtk )
     int i, k;
     // set the PI numbers
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pNext = (void *)i;
+        pObj->pNext = (void *)(PORT_PTRINT_T)i;
     // save the CI numbers
     vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
@@ -427,7 +427,7 @@ Vec_Ptr_t * Abc_NtkComputeSupportsNaive( Abc_Ntk_t * pNtk )
         vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
         vSuppI = (Vec_Int_t *)vSupp;
         Vec_PtrForEachEntry( vSupp, pTemp, k )
-            Vec_IntWriteEntry( vSuppI, k, (int)pTemp->pNext );
+            Vec_IntWriteEntry( vSuppI, k, (int)(PORT_PTRINT_T)pTemp->pNext );
         Vec_IntSort( vSuppI, 0 );
         // append the number of this output
         Vec_IntPush( vSuppI, i );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 271f94df..b753700e 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -80,11 +80,11 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
     ParsNew.nPis  = Abc_NtkPiNum( pNtk );
     ParsNew.nPos  = Abc_NtkPoNum( pNtk );
     // reset the parameters if the network has the same name
-    if ( ParsBest.pName == NULL || 
-         strcmp(ParsBest.pName, pNtk->pName) ||
-         ParsBest.Depth >  ParsNew.Depth || 
-         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops || 
-         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes )
+    if (  ParsBest.pName == NULL ||
+          strcmp(ParsBest.pName, pNtk->pName) ||
+          ParsBest.Depth >  ParsNew.Depth ||
+         (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops) ||
+         (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes) )
     {
         FREE( ParsBest.pName );
         ParsBest.pName = Extra_UtilStrsav( pNtk->pName );
@@ -145,9 +145,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
     else if ( Abc_NtkIsStrash(pNtk) )
     {        
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
-        if ( Num = Abc_NtkGetChoiceNum(pNtk) )
+        if ( (Num = Abc_NtkGetChoiceNum(pNtk)) )
             fprintf( pFile, " (choice = %d)", Num );
-        if ( Num = Abc_NtkGetExorNum(pNtk) )
+        if ( (Num = Abc_NtkGetExorNum(pNtk)) )
             fprintf( pFile, " (exor = %d)", Num );
 //        if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
 //            fprintf( pFile, " (mux = %d)", Num2-Num );
@@ -930,7 +930,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
         return;
 
     // transform logic functions from BDD to SOP
-    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+    if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
         {
@@ -955,9 +955,11 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
             CountBuf++;
         else if ( Abc_SopIsInv(pSop) )
             CountInv++;
-        else if ( !Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop) ||  Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop) )
+        else if ( (!Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop)) ||
+                  ( Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop)) )
             CountAnd++;
-        else if (  Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop) || !Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop) )
+        else if ( ( Abc_SopIsComplement(pSop) && Abc_SopIsAndType(pSop)) ||
+                  (!Abc_SopIsComplement(pSop) && Abc_SopIsOrType(pSop)) )
             CountOr++;
         else
             CountOther++;
@@ -1127,7 +1129,7 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
 */
     // print the logic function
     if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) )
-        fprintf( pFile, " %s", pObj->pData );
+        fprintf( pFile, " %s", (char*)pObj->pData );
     else
         fprintf( pFile, "\n" );
 }
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 618b6a0f..6a695fc4 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -55,7 +55,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
     Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int RetValue, nIter, nSatFails, Counter, clk, timeStart = clock();
+    int RetValue = -1, nIter, nSatFails, Counter, clk; //, timeStart = clock();
     sint64 nSatConfs, nSatInspects, nInspectLimit;
 
     // get the starting network
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 42494b5c..815e452a 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -132,10 +132,10 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde
 DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
 {
     int fInternalReorder = 0;
-    Extra_ImageTree_t * pTree;
-    Extra_ImageTree2_t * pTree2;
+    Extra_ImageTree_t * pTree = NULL;
+    Extra_ImageTree2_t * pTree2 = NULL;
     DdNode * bReached, * bCubeCs;
-    DdNode * bCurrent, * bNext, * bTemp;
+    DdNode * bCurrent, * bNext = NULL, * bTemp;
     DdNode ** pbVarsY;
     Abc_Obj_t * pLatch;
     int i, nIters, nBddSize;
@@ -159,6 +159,7 @@ DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pb
     // perform reachability analisys
     bCurrent = bInitial;   Cudd_Ref( bCurrent );
     bReached = bInitial;   Cudd_Ref( bReached );
+    assert( nIterMax > 1 ); // required to not deref uninitialized bNext
     for ( nIters = 1; nIters <= nIterMax; nIters++ )
     {
         // compute the next states
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index f74cbee8..2983efc2 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -232,11 +232,6 @@ p->timeTruth += clock() - clk;
         pObj = Abc_ObjFanin0(pObj);
         pTruth = Vec_PtrEntry( p->vTtNodes, pObj->Id );
 
-        if ( pTruth[0] == 1128481603 )
-        {
-            int x = 0;
-        }
-
         // add the resulting truth table to the hash table 
         ppSpot = Abc_NtkRecTableLookup( p, pTruth, p->nVars );
         assert( pObj->pEquiv == NULL );
@@ -777,7 +772,7 @@ int Abc_NtkRecAddCut( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
     static int s_MaxSize[16] = { 0 };
     char Buffer[40], Name[20], Truth[20];
     char pCanonPerm[16];
-    Abc_Obj_t * pObj, * pFanin0, * pFanin1, ** ppSpot, * pObjPo;
+    Abc_Obj_t * pObj = NULL, * pFanin0, * pFanin1, ** ppSpot, * pObjPo;
     Abc_Ntk_t * pAig = s_pMan->pNtk;
     If_Obj_t * pIfObj;
     Vec_Ptr_t * vNodes = s_pMan->vNodes;
@@ -788,11 +783,6 @@ int Abc_NtkRecAddCut( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
     unsigned uCanonPhase;
     int clk;
 
-    if ( pRoot->Id == 2639 )
-    {
-        int y = 0;
-    }
-
     assert( nInputs <= 16 );
     assert( nInputs == (int)pCut->nLimit );
     s_pMan->nTried++;
@@ -848,7 +838,7 @@ s_pMan->timeCanon += clock() - clk;
     for ( i = 0; i < nLeaves; i++ )
     {
         // get hold of the corresponding leaf
-        pIfObj = If_ManObj( pIfMan, pCut->pLeaves[pCanonPerm[i]] );
+        pIfObj = If_ManObj( pIfMan, pCut->pLeaves[(int)pCanonPerm[i]] );
         // get hold of the corresponding new node
         pObj = Abc_NtkPi( pAig, i );
         pObj = Abc_ObjNotCond( pObj, (uCanonPhase & (1 << i)) );
@@ -897,6 +887,7 @@ s_pMan->timeCanon += clock() - clk;
         }
     }
 
+    assert(pObj);
     pTruth = Vec_PtrEntry( s_pMan->vTtNodes, pObj->Id );
     if ( Kit_TruthSupport(pTruth, nInputs) != Kit_BitMask(nLeaves) )
     {
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index e77f055a..078aee9d 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -384,8 +384,8 @@ int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int
 ***********************************************************************/
 int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
 {
-    Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
-    int CostCur, i;
+    Abc_Obj_t * pNode = NULL, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
+    int CostCur = 0, i;
     // find the best fanin
     Vec_PtrForEachEntry( vLeaves, pNode, i )
     {
@@ -494,7 +494,7 @@ void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
 DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
 {
     Abc_Obj_t * pNode;
-    DdNode * bFunc0, * bFunc1, * bFunc;
+    DdNode * bFunc0, * bFunc1, * bFunc = NULL;
     int i;
     // get the nodes in the cut without fanins in the DFS order
     Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
@@ -510,6 +510,7 @@ DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, V
         bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
         pNode->pCopy = (Abc_Obj_t *)bFunc;
     }
+    assert(bFunc);
     Cudd_Ref( bFunc );
     // dereference the intermediate ones
     Vec_PtrForEachEntry( vVisited, pNode, i )
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index b925f1b9..821bd66b 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -267,7 +267,7 @@ clk = clock();
     nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required );
 p->timeEval += clock() - clk;
     // quit if there is no improvement
-    if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros )
+    if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) )
     {
         Cudd_RecursiveDeref( p->dd, bNodeFunc );
         Dec_GraphFree( pFForm );
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index aa9a2998..2550e02c 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -295,7 +295,7 @@ Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_
     {
         if ( pCut->nLeaves < 4 )
             continue;
-        if ( pGraph = Abc_NodeRestructureCut( p, pNode, pCut ) )
+        if ( (pGraph = Abc_NodeRestructureCut( p, pNode, pCut )) )
             return pGraph;
     }
     return NULL;
@@ -337,11 +337,6 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C
         Vec_PtrPush( p->vLeaves, pLeaf );
     }
 
-    if ( pRoot->Id == 29 )
-    {
-        int x = 0;
-    }
-
 clk = clock();
     // collect the internal nodes of the cut
 //    Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
@@ -430,7 +425,7 @@ clk = clock();
 p->timeEval += clock() - clk;
 
     // quit if there is no improvement
-    if ( pGraph == NULL || nNodesAdded == -1 || nNodesAdded == nNodesSaved && !p->fUseZeros )
+    if ( pGraph == NULL || nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !p->fUseZeros) )
     {
         Cudd_RecursiveDeref( p->dd, bFunc );
         if ( pGraph ) Dec_GraphFree( pGraph );
@@ -1206,16 +1201,16 @@ void Abc_NodeMffcSimulate( Vec_Ptr_t * vDecs, int nLeaves, Vec_Int_t * vRands, V
     Vec_PtrForEachEntryStop( vDecs, pObj, i, nLeaves )
     {
         uData = (unsigned)Vec_IntEntry( vRands, i );
-        pObj->pData = (void *)uData;
+        pObj->pData = (void *)(PORT_PTRUINT_T)uData;
         Vec_IntPush( vSims, uData );
     }
     // simulate
     Vec_PtrForEachEntryStart( vDecs, pObj, i, nLeaves )
     {
-        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
+        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData = (Abc_ObjFaninC0(pObj)? ~uData0 : uData0) & (Abc_ObjFaninC1(pObj)? ~uData1 : uData1);
-        pObj->pData = (void *)uData;
+        pObj->pData = (void *)(PORT_PTRUINT_T)uData;
         Vec_IntPush( vSims, uData );
     }
 }
@@ -1248,7 +1243,7 @@ int Abc_NodeCheckFull( Abc_ManRst_t * p, Dec_Graph_t * pGraph )
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeMffcConstants( Abc_ManRst_t * p, Vec_Int_t * vSims )
 {
-    Dec_Graph_t * pGraph;
+    Dec_Graph_t * pGraph = NULL;
     unsigned uRoot;
     // get the root node
     uRoot = (unsigned)Vec_IntEntryLast( vSims );
@@ -1258,6 +1253,7 @@ Dec_Graph_t * Abc_NodeMffcConstants( Abc_ManRst_t * p, Vec_Int_t * vSims )
     else if ( uRoot == ~(unsigned)0 )
         pGraph = Dec_GraphCreateConst1();
     // check the graph
+    assert(pGraph);
     if ( Abc_NodeCheckFull( p, pGraph ) )
         return pGraph;
     Dec_GraphFree( pGraph );
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index a2b23c0c..80532b14 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -164,9 +164,10 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
     if ( fUpdateLevel )
         Abc_NtkStartReverseLevels( pNtk, 0 );
 
-    if ( Abc_NtkLatchNum(pNtk) )
+    if ( Abc_NtkLatchNum(pNtk) ) {
         Abc_NtkForEachLatch(pNtk, pNode, i)
             pNode->pNext = pNode->pData;
+    }
 
     // resynthesize each node once
     pManRes->nNodesBeg = Abc_NtkNodeNum(pNtk);
@@ -249,9 +250,10 @@ pManRes->timeTotal = clock() - clkStart;
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->pData = NULL;
 
-    if ( Abc_NtkLatchNum(pNtk) )
+    if ( Abc_NtkLatchNum(pNtk) ) {
         Abc_NtkForEachLatch(pNtk, pNode, i)
             pNode->pData = pNode->pNext, pNode->pNext = NULL;
+    }
 
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
@@ -1131,7 +1133,7 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
 ***********************************************************************/
 Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
 {
-    Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObjMax, * pObjMin0, * pObjMin1;
+    Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObjMax, * pObjMin0 = NULL, * pObjMin1 = NULL;
     unsigned * puData0, * puData1, * puData2, * puDataR;
     int i, k, j, w, LevelMax;
     puDataR = p->pRoot->pData;
@@ -1169,6 +1171,8 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
                     }
 
                     p->nUsedNode2Or++;
+                    assert(pObjMin0);
+                    assert(pObjMin1);
                     return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 1 );
                 }
             }
@@ -1208,6 +1212,8 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
                     }
 
                     p->nUsedNode2And++;
+                    assert(pObjMin0);
+                    assert(pObjMin1);
                     return Abc_ManResubQuit21( p->pRoot, pObjMin0, pObjMin1, pObjMax, 0 );
                 }
             }
@@ -1341,7 +1347,7 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required )
 {
     Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObj3;
     unsigned * puData0, * puData1, * puData2, * puData3, * puDataR;
-    int i, k, w, Flag;
+    int i, k, w = 0, Flag;
     puDataR = p->pRoot->pData;
     // check positive unate divisors
     Vec_PtrForEachEntry( p->vDivs2UP0, pObj0, i )
@@ -1653,7 +1659,7 @@ p->timeSim += clock() - clk;
 
 clk = clock();
     // consider constants
-    if ( pGraph = Abc_ManResubQuit( p ) )
+    if ( (pGraph = Abc_ManResubQuit( p )) )
     {
         p->nUsedNodeC++;
         p->nLastGain = p->nMffc;
@@ -1661,7 +1667,7 @@ clk = clock();
     }
 
     // consider equal nodes
-    if ( pGraph = Abc_ManResubDivs0( p ) )
+    if ( (pGraph = Abc_ManResubDivs0( p )) )
     {
 p->timeRes1 += clock() - clk;
         p->nUsedNode0++;
@@ -1678,7 +1684,7 @@ p->timeRes1 += clock() - clk;
     Abc_ManResubDivsS( p, Required );
 
     // consider one node
-    if ( pGraph = Abc_ManResubDivs1( p, Required ) )
+    if ( (pGraph = Abc_ManResubDivs1( p, Required )) )
     {
 p->timeRes1 += clock() - clk;
         p->nLastGain = p->nMffc - 1;
@@ -1690,7 +1696,7 @@ p->timeRes1 += clock() - clk;
 
 clk = clock();
     // consider triples
-    if ( pGraph = Abc_ManResubDivs12( p, Required ) )
+    if ( (pGraph = Abc_ManResubDivs12( p, Required )) )
     {
 p->timeRes2 += clock() - clk;
         p->nLastGain = p->nMffc - 2;
@@ -1705,7 +1711,7 @@ p->timeResD += clock() - clk;
 
     // consider two nodes
 clk = clock();
-    if ( pGraph = Abc_ManResubDivs2( p, Required ) )
+    if ( (pGraph = Abc_ManResubDivs2( p, Required )) )
     {
 p->timeRes2 += clock() - clk;
         p->nLastGain = p->nMffc - 2;
@@ -1717,7 +1723,7 @@ p->timeRes2 += clock() - clk;
 
     // consider two nodes
 clk = clock();
-    if ( pGraph = Abc_ManResubDivs3( p, Required ) )
+    if ( (pGraph = Abc_ManResubDivs3( p, Required )) )
     {
 p->timeRes3 += clock() - clk;
         p->nLastGain = p->nMffc - 3;
@@ -1880,7 +1886,7 @@ Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax )
     vFeasible = Vec_IntAlloc( nLeavesMax );
     while ( 1 )
     {
-        BestCut = -1;
+        BestCut = -1, BestShare = -1;
         // find the next feasible cut to add
         Vec_IntClear( vFeasible );
         Vec_PtrForEachEntry( vFactors, vFact, i )
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 3b50107b..ff1e1f8b 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -62,7 +62,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
     Cut_Man_t * pManCut;
     Rwr_Man_t * pManRwr;
     Abc_Obj_t * pNode;
-    Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
+//    Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
     Dec_Graph_t * pGraph;
     int i, nNodes, nGain, fCompl;
     int clk, clkStart = clock();
@@ -120,7 +120,7 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
 
         // for each cut, try to resynthesize it
         nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros, fPlaceEnable );
-        if ( !(nGain > 0 || nGain == 0 && fUseZeros) )
+        if ( !(nGain > 0 || (nGain == 0 && fUseZeros)) )
             continue;
         // if we end up here, a rewriting step is accepted
 
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index c33444df..888850e1 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -729,16 +729,16 @@ void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk )
     int i;
     Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0);
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pData = (void *)SIM_RANDOM_UNSIGNED;
+        pObj->pData = (void *)(PORT_PTRUINT_T)SIM_RANDOM_UNSIGNED;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) continue;
-        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
+        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
         assert( pObj->pData == NULL );
-        pObj->pData = (void *)uData;
+        pObj->pData = (void *)(PORT_PTRUINT_T)uData;
     }
 }
 
@@ -802,24 +802,24 @@ Vec_Str_t * Abc_NtkRRSimulate( Abc_Ntk_t * pNtk )
     // simulate patters and store them in copy
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0);
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)SIM_RANDOM_UNSIGNED;
+        pObj->pCopy = (Abc_Obj_t *)(PORT_PTRUINT_T)SIM_RANDOM_UNSIGNED;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( i == 0 ) continue;
-        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
-        uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
+        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pData;
         uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
         uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
-        pObj->pCopy = (Abc_Obj_t *)uData;
+        pObj->pCopy = (Abc_Obj_t *)(PORT_PTRUINT_T)uData;
     }
     // store the result in data
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
+        uData0 = (unsigned)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData;
         if ( Abc_ObjFaninC0(pObj) )
-            pObj->pData = (void *)~uData0;
+            pObj->pData = (void *)(PORT_PTRUINT_T)~uData0;
         else
-            pObj->pData = (void *)uData0;
+            pObj->pData = (void *)(PORT_PTRUINT_T)uData0;
     }
 
     // refine the candidates
@@ -904,7 +904,7 @@ void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField )
     Abc_ObjForEachFanin( pRoot, pFanin, i )
         Sim_CollectNodes_rec( pFanin, vField );
     if ( !Abc_ObjIsCo(pRoot) )
-        pRoot->pData = (void *)Vec_PtrSize(vField);
+        pRoot->pData = (void *)(PORT_PTRUINT_T)Vec_PtrSize(vField);
     Vec_PtrPush( vField, pRoot );
 }
 
@@ -934,13 +934,13 @@ void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t
         {
             pUnsigned = Vec_PtrEntry( vSims, i );
             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
-                pUnsigned[k] = (unsigned)pObj->pCopy;
+                pUnsigned[k] = (unsigned)(PORT_PTRUINT_T)pObj->pCopy;
             continue;
         }
         if ( Abc_ObjIsCo(pObj) )
         {
             pUnsigned  = Vec_PtrEntry( vSims, i );
-            pUnsignedF = Vec_PtrEntry( vSims, (int)Abc_ObjFanin0(pObj)->pData );
+            pUnsignedF = Vec_PtrEntry( vSims, (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pData );
             if ( Abc_ObjFaninC0(pObj) )
                 for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
                     pUnsigned[k] = ~pUnsignedF[k];
@@ -950,7 +950,7 @@ void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t
             // update targets
             for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
             {
-                if ( pUnsigned[k] == (unsigned)pObj->pData )
+                if ( pUnsigned[k] == (unsigned)(PORT_PTRUINT_T)pObj->pData )
                     continue;
                 pDisproved = Vec_PtrEntry( vNodes, k );
                 fCompl = Abc_ObjIsComplement(pDisproved);
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index afdfbdeb..025652fe 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -27,7 +27,7 @@
 
 static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
 extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
-static nMuxes;
+static int nMuxes;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -151,7 +151,7 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk )
     int i;
     vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
     Abc_NtkForEachCi( pNtk, pObj, i )
-        Vec_IntPush( vCiIds, (int)pObj->pCopy );
+        Vec_IntPush( vCiIds, (int)(PORT_PTRINT_T)pObj->pCopy );
     return vCiIds;
 }
 
@@ -172,7 +172,7 @@ int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
 {
 //printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
-    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+    Vec_IntPush( vVars, toLitCond( (int)(PORT_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
     return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
@@ -195,7 +195,7 @@ int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
 //printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->sat_solver_stats.clauses );
     vVars->nSize = 0;
     Vec_PtrForEachEntry( vNodes, pNode, i )
-        Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+        Vec_IntPush( vVars, toLitCond( (int)(PORT_PTRINT_T)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
 //    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
     return sat_solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
@@ -220,7 +220,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
     assert( Abc_ObjIsNode( pNode ) );
 
 //    nVars = sat_solver_nvars(pSat);
-    Var = (int)pNode->pCopy;
+    Var = (int)(PORT_PTRINT_T)pNode->pCopy;
 //    Var = pNode->Id;
 
 //    assert( Var  < nVars ); 
@@ -230,7 +230,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
         // get the complemented attributes of the nodes
         fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
         // determine the variable numbers
-        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+        Var1 = (int)(PORT_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
 //        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
 
         // check that the variables are in the SAT manager
@@ -255,7 +255,7 @@ int Abc_NtkClauseAnd( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Ptr_t * vSuper,
         // get the complemented attributes of the nodes
         fComp1 = Abc_ObjIsComplement(vSuper->pArray[i]);
         // determine the variable numbers
-        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
+        Var1 = (int)(PORT_PTRINT_T)Abc_ObjRegular(vSuper->pArray[i])->pCopy;
 //        Var1 = (int)Abc_ObjRegular(vSuper->pArray[i])->Id;
         // add this variable to the array
         Vec_IntPush( vVars, toLitCond(Var1, !fComp1) );
@@ -283,10 +283,10 @@ int Abc_NtkClauseMux( sat_solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC,
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_NodeIsMuxType( pNode ) );
     // get the variable numbers
-    VarF = (int)pNode->pCopy;
-    VarI = (int)pNodeC->pCopy;
-    VarT = (int)Abc_ObjRegular(pNodeT)->pCopy;
-    VarE = (int)Abc_ObjRegular(pNodeE)->pCopy;
+    VarF = (int)(PORT_PTRINT_T)pNode->pCopy;
+    VarI = (int)(PORT_PTRINT_T)pNodeC->pCopy;
+    VarT = (int)(PORT_PTRINT_T)Abc_ObjRegular(pNodeT)->pCopy;
+    VarE = (int)(PORT_PTRINT_T)Abc_ObjRegular(pNodeE)->pCopy;
 //    VarF = (int)pNode->Id;
 //    VarI = (int)pNodeC->Id;
 //    VarT = (int)Abc_ObjRegular(pNodeT)->Id;
@@ -379,12 +379,12 @@ int Abc_NtkCollectSupergate_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, int fFir
     }
     // if the new node is complemented or a PI, another gate begins
     if ( !fFirst )
-    if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || fStopAtMux && Abc_NodeIsMuxType(pNode) )
-    {
-        Vec_PtrPush( vSuper, pNode );
-        Abc_ObjRegular(pNode)->fMarkB = 1;
-        return 0;
-    }
+        if ( Abc_ObjIsComplement(pNode) || !Abc_ObjIsNode(pNode) || Abc_ObjFanoutNum(pNode) > 1 || (fStopAtMux && Abc_NodeIsMuxType(pNode)) )
+        {
+            Vec_PtrPush( vSuper, pNode );
+            Abc_ObjRegular(pNode)->fMarkB = 1;
+            return 0;
+        }
     assert( !Abc_ObjIsComplement(pNode) );
     assert( Abc_ObjIsNode(pNode) );
     // go through the branches
@@ -462,9 +462,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vNodes, * vSuper;
     Vec_Int_t * vVars;
     int i, k, fUseMuxes = 1;
-    int clk1 = clock();
 //    int fOrderCiVarsFirst = 0;
-    int nLevelsMax = Abc_AigLevel(pNtk);
     int RetValue = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -481,7 +479,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
     // add the clause for the constant node
     pNode = Abc_AigConst1(pNtk);
     pNode->fMarkA = 1;
-    pNode->pCopy = (Abc_Obj_t *)vNodes->nSize;
+    pNode->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
     Vec_PtrPush( vNodes, pNode );
     Abc_NtkClauseTriv( pSat, pNode, vVars );
 /*
@@ -503,7 +501,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
         if ( pFanin->fMarkA == 0 )
         {
             pFanin->fMarkA = 1;
-            pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+            pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
             Vec_PtrPush( vNodes, pFanin );
         }
         // add the trivial clause
@@ -538,7 +536,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 if ( pFanin->fMarkA == 0 )
                 {
                     pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+                    pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
                     Vec_PtrPush( vNodes, pFanin );
                 }
             }
@@ -557,7 +555,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 if ( pFanin->fMarkA == 0 )
                 {
                     pFanin->fMarkA = 1;
-                    pFanin->pCopy = (Abc_Obj_t *)vNodes->nSize;
+                    pFanin->pCopy = (Abc_Obj_t *)(PORT_PTRINT_T)vNodes->nSize;
                     Vec_PtrPush( vNodes, pFanin );
                 }
             }
@@ -625,7 +623,7 @@ void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
 {
     sat_solver * pSat;
     Abc_Obj_t * pNode;
-    int RetValue, i, clk = clock();
+    int RetValue, i; //, clk = clock();
 
     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsBddLogic(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
@@ -842,7 +840,7 @@ sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
 
     // transfer the IDs to the copy field
     Abc_NtkForEachPi( pNtk, pNode, i )
-        pNode->pCopy = (void *)pNode->Id;
+        pNode->pCopy = (void *)(PORT_PTRINT_T)pNode->Id;
 
     // start the data structures
     pSat    = sat_solver_new();
@@ -913,7 +911,7 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
 
     if ( nQueens <= 0 && nQueens >= nVars )
     {
-        printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens, nVars );
+        printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens);
         return;
     }
     assert( nQueens > 0 && nQueens < nVars );
@@ -947,9 +945,9 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pCopy = (void *)~0;
     Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->pCopy = (void *)Counter++;
+        pObj->pCopy = (void *)(PORT_PTRINT_T)Counter++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)Counter++;
+        pObj->pCopy = (void *)(PORT_PTRINT_T)Counter++;
 
 /*
         OutVar   = pCnf->pVarNums[ pObj->Id ];
@@ -977,14 +975,14 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // positive phase
-        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)pObj->pCopy, 
-            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)Abc_ObjFanin0(pObj)->pCopy,
-            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)(PORT_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy,
+            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
         // negative phase
-        fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy, 
-            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)Abc_ObjFanin0(pObj)->pCopy );
-        fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy, 
-            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(PORT_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n",     1+(int)(PORT_PTRINT_T)pObj->pCopy,
+            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy );
     }
     Vec_PtrFree( vNodes );
 
@@ -994,10 +992,10 @@ void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
 */
     // assert the first literal to zero
     fprintf( pFile, "%s%d 0\n", 
-        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)Abc_ObjFanin0(ppNodes[0])->pCopy );
+        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(ppNodes[0])->pCopy );
     // assert the second literal to one
     fprintf( pFile, "%s%d 0\n", 
-        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)Abc_ObjFanin0(ppNodes[1])->pCopy );
+        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)(PORT_PTRINT_T)Abc_ObjFanin0(ppNodes[1])->pCopy );
     fclose( pFile );
 }
 
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index c1e0faf0..084f6a6c 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -46,7 +46,7 @@ static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, int fAl
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
 {
-    extern int timeRetime;
+//    extern int timeRetime;
     Abc_Ntk_t * pNtkAig;
     Abc_Obj_t * pObj;
     int i, nNodes;//, RetValue;
@@ -99,7 +99,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
 {
-    extern int timeRetime;
+//    extern int timeRetime;
     Abc_Ntk_t * pNtkAig;
     Abc_Obj_t * pObj;
     int i, nNodes;//, RetValue;
@@ -311,7 +311,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, int fAllNod
     ProgressBar * pProgress;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNodeOld;
-    int i, clk = clock();
+    int i; //, clk = clock();
     assert( Abc_NtkIsLogic(pNtkOld) );
     assert( Abc_NtkIsStrash(pNtkNew) );
 //    vNodes = Abc_NtkDfs( pNtkOld, fAllNodes );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 1ae8745b..c5f4bb1e 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -338,9 +338,9 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
 //        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
 //        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
         if (  Arrival1 > Arrival2 ||
-              Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level || 
-              Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && 
-              Abc_NodeDroppingCost(pNodeMin) < Abc_NodeDroppingCost(pNode)  )
+              (Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level) ||
+              (Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level &&
+              Abc_NodeDroppingCost(pNodeMin) < Abc_NodeDroppingCost(pNode))  )
             pNodeMin = pNode;
     }
 
@@ -358,9 +358,9 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
 //        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
 //        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
         if (  Arrival1 > Arrival2 ||
-              Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level || 
-              Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && 
-              Abc_NodeDroppingCost(pNodeMin) < Abc_NodeDroppingCost(pNode)  )
+              (Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level) ||
+              (Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level &&
+              Abc_NodeDroppingCost(pNodeMin) < Abc_NodeDroppingCost(pNode))  )
             pNodeMin = pNode;
     }
 
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 96a4566d..1131f119 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -669,18 +669,18 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
     // set the CI values
     Abc_AigConst1(pNtk)->pCopy = (void *)1;
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (void *)pModel[i];
+        pNode->pCopy = (void *)(PORT_PTRINT_T)pModel[i];
     // simulate in the topological order
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
-        Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
-        pNode->pCopy = (void *)(Value0 & Value1);
+        Value0 = ((int)(PORT_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+        Value1 = ((int)(PORT_PTRINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
+        pNode->pCopy = (void *)(PORT_PTRINT_T)(Value0 & Value1);
     }
     // fill the output values
     pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
-        pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+        pValues[i] = ((int)(PORT_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
     if ( fStrashed )
         Abc_NtkDelete( pNtk );
     return pValues;
@@ -740,7 +740,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
         vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
         // set the PI numbers
         Abc_NtkForEachCi( pNtk1, pNode, i )
-            pNode->pCopy = (void*)i;
+            pNode->pCopy = (void*)(PORT_PTRINT_T)i;
         // print the model
         pNode = Vec_PtrEntry( vNodes, 0 );
         if ( Abc_ObjIsCi(pNode) )
@@ -748,7 +748,7 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
             Vec_PtrForEachEntry( vNodes, pNode, i )
             {
                 assert( Abc_ObjIsCi(pNode) );
-                printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] );
+                printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)(PORT_PTRINT_T)pNode->pCopy] );
             }
         }
         printf( "\n" );
@@ -819,9 +819,9 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
 {
     Vec_Ptr_t * vInfo1, * vInfo2;
     Abc_Obj_t * pObj, * pObjError, * pObj1, * pObj2;
-    int ValueError1, ValueError2;
+    int ValueError1 = -1, ValueError2 = -1;
     unsigned * pPats1, * pPats2;
-    int i, o, k, nErrors, iFrameError, iNodePo, nPrinted;
+    int i, o, k, nErrors, iFrameError = -1, iNodePo = -1, nPrinted;
     int fRemove1 = 0, fRemove2 = 0;
 
     if ( !Abc_NtkIsStrash(pNtk1) )
@@ -991,7 +991,7 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
     Abc_NtkForEachPi( pNtk, pObj, i )
         pModel1[i] = vPiValues1[i] - '0';
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)pObj->pData) - 1;
+        pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)(PORT_PTRINT_T)pObj->pData) - 1;
 
     pResult1 = Abc_NtkVerifySimulatePattern( pNtk, pModel1 );
     printf( "Value = %d\n", pResult1[0] );
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index e5656170..87739572 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -28,8 +28,8 @@
 #define XVS1   ABC_INIT_ONE
 #define XVSX   ABC_INIT_DC
 
-static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)Value;  }
-static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)pObj->pCopy;      }
+static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)(PORT_PTRINT_T)Value;  }
+static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)(PORT_PTRINT_T)pObj->pCopy;      }
 static inline int  Abc_XsimInv( int Value )   
 { 
     if ( Value == XVS0 )
@@ -214,7 +214,7 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     }
     // set the final values
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pData = (void *)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
+        pObj->pData = (void *)(PORT_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
 }
 
 ///////////////////////////////////////////////////////////////////////
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 313ae0ed..75aa0064 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -20,6 +20,8 @@
  
 #ifdef WIN32
 #include <process.h> 
+#else
+#include <unistd.h>
 #endif
 
 #include "mainInt.h"
@@ -346,7 +348,7 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
     size = pAbc->aHistory->nSize;
     num = ( num < size ) ? num : size;
     for ( i = size - num; i < size; i++ )
-        fprintf( pAbc->Out, "%s", pAbc->aHistory->pArray[i] );
+        fprintf( pAbc->Out, "%s", (char*)pAbc->aHistory->pArray[i] );
     return 0;
 
 usage:
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 7538e31c..1695942e 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -970,7 +970,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( pFileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", pFileName );
-        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" )) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", pFileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -1061,7 +1061,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( pFileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", pFileName );
-        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" )) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", pFileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -1120,6 +1120,11 @@ int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1168,6 +1173,11 @@ int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 2 )
         goto usage;
     // get the output file name
@@ -1226,6 +1236,11 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1276,6 +1291,11 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1319,6 +1339,11 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1362,6 +1387,11 @@ int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1410,6 +1440,11 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1467,14 +1502,14 @@ int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
-    if ( argc != globalUtilOptind + 1 )
-        goto usage;
-    pNtk = pAbc->pNtkCur;
-    if ( pNtk == NULL )
+    if ( pAbc->pNtkCur == NULL )
     {
         fprintf( pAbc->Out, "Empty network.\n" );
         return 0;
     }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    pNtk = pAbc->pNtkCur;
     // get the output file name
     pFileName = argv[globalUtilOptind];
     // call the corresponding file writer
@@ -1532,6 +1567,11 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1588,6 +1628,11 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1763,6 +1808,11 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1806,6 +1856,11 @@ int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1857,13 +1912,13 @@ int IoCommandWriteList( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
-    if ( argc != globalUtilOptind + 1 )
-        goto usage;
     if ( pAbc->pNtkCur == NULL )
     {
         fprintf( pAbc->Out, "Empty network.\n" );
         return 0;
     }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
 /*
     if ( !Abc_NtkIsSeq(pAbc->pNtkCur) )
     {
@@ -1913,6 +1968,11 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
@@ -1956,6 +2016,11 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
                 goto usage;
         }
     }
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
     if ( argc != globalUtilOptind + 1 )
         goto usage;
     // get the output file name
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 9ecc00fd..b8555561 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -19,8 +19,11 @@
 
 ***********************************************************************/
 
+// The code in this file is developed in collaboration with Mark Jarvin of Toronto.
+
 #include "ioAbc.h"
-#include <bzlib.h>
+#include "bzlib.h"
+#include "zlib.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -104,7 +107,7 @@ typedef struct buflist {
   struct buflist * next;
 } buflist;
 
-static char * Ioa_ReadLoadFileBz2Aig( char * pFileName )
+static char * Ioa_ReadLoadFileBz2Aig( char * pFileName, int * pFileSize )
 {
     FILE    * pFile;
     int       nFileSize = 0;
@@ -168,12 +171,48 @@ static char * Ioa_ReadLoadFileBz2Aig( char * pFileName )
     fclose( pFile );
     // finish off the file with the spare .end line
     // some benchmarks suddenly break off without this line
-    strcpy( pContents + nFileSize, "\n.end\n" );
+//    strcpy( pContents + nFileSize, "\n.end\n" );
+    *pFileSize = nFileSize;
     return pContents;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Reads the file into a character buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Ioa_ReadLoadFileGzAig( char * pFileName, int * pFileSize )
+{
+    const int READ_BLOCK_SIZE = 100000;
+    FILE * pFile;
+    char * pContents;
+    int amtRead, readBlock, nFileSize = READ_BLOCK_SIZE;
+    pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
+    pContents = ALLOC( char, nFileSize );        
+    readBlock = 0;
+    while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) {
+        //printf("%d: read %d bytes\n", readBlock, amtRead);
+        nFileSize += READ_BLOCK_SIZE;
+        pContents = REALLOC(char, pContents, nFileSize);
+        ++readBlock;
+    }
+    //printf("%d: read %d bytes\n", readBlock, amtRead);
+    assert( amtRead != -1 ); // indicates a zlib error
+    nFileSize -= (READ_BLOCK_SIZE - amtRead);
+    gzclose(pFile);
+    *pFileSize = nFileSize;
+    return pContents;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Reads the AIG in the binary AIGER format.]
 
   Description []
@@ -191,13 +230,15 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     Vec_Int_t * vLits = NULL;
     Abc_Obj_t * pObj, * pNode0, * pNode1;
     Abc_Ntk_t * pNtkNew;
-    int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
-    char * pContents, * pDrivers, * pSymbols, * pCur, * pName, * pType;
+    int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize = -1, iTerm, nDigits, i;
+    char * pContents, * pDrivers = NULL, * pSymbols, * pCur, * pName, * pType;
     unsigned uLit0, uLit1, uLit;
 
     // read the file into the buffer
     if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) )
-        pContents = Ioa_ReadLoadFileBz2Aig( pFileName );
+        pContents = Ioa_ReadLoadFileBz2Aig( pFileName, &nFileSize );
+    else if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) )
+        pContents = Ioa_ReadLoadFileGzAig( pFileName, &nFileSize );
     else
     {
 //        pContents = Ioa_ReadLoadFile( pFileName );
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 13f644cc..eb337603 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -112,9 +112,9 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
     }
 
     // get the pointer to the beginning of the node array
-    pBufferNode = (int *)(pContents + (nFileSize - (2 * nAnds + nOutputs + nLatches) * sizeof(int)) );
+    pBufferNode = (unsigned *)(pContents + (nFileSize - (2 * nAnds + nOutputs + nLatches) * sizeof(int)) );
     // make sure we are at the place where the nodes begin
-    if ( pBufferNode != (int *)pCur )
+    if ( pBufferNode != (unsigned *)pCur )
     {
         free( pContents );
         Vec_PtrFree( vNodes );
@@ -140,7 +140,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
         Num = pBufferNode[2*nAnds+i];
         if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) )
         {
-            Abc_ObjSetData( Abc_ObjFanout0(pObj), (void *)(Num & 3) );
+            Abc_ObjSetData( Abc_ObjFanout0(pObj), (void *)(PORT_PTRINT_T)(Num & 3) );
             Num >>= 2;
         }
         pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, Num >> 1), Num & 1 );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 0742ec1f..b6e0e15f 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -95,7 +95,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
     // go through the lines of the file
     vString = Vec_StrAlloc( 100 );
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
-    for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+    for ( iLine = 0; (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
     {
         Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 68a0bc35..c818cd55 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -206,7 +206,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
 ***********************************************************************/
 Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
 {
-    ProgressBar * pProgress;
+    ProgressBar * pProgress = NULL;
     Abc_Ntk_t * pNtk;
     char * pDirective;
     int iLine, fTokensReady, fStatus;
@@ -235,7 +235,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) 
     {
         printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, 
-            Extra_FileReaderGetLineNumber(p->pReader, 0), p->vTokens->pArray[0] );
+            Extra_FileReaderGetLineNumber(p->pReader, 0), (char*)p->vTokens->pArray[0] );
         Abc_NtkDelete(pNtk);
         p->pNtkCur = NULL;
         return NULL;
@@ -243,12 +243,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
 
     // read the inputs/outputs
     if ( p->pNtkMaster == NULL )
-    pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
+        pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
     fTokensReady = fStatus = 0;
     for ( iLine = 0; fTokensReady || (p->vTokens = Io_ReadBlifGetTokens(p)); iLine++ )
     {
         if ( p->pNtkMaster == NULL && iLine % 1000 == 0 )
-        Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p->pReader), NULL );
+            Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p->pReader), NULL );
 
         // consider different line types
         fTokensReady = 0;
@@ -298,7 +298,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         }
     }
     if ( p->pNtkMaster == NULL )
-    Extra_ProgressBarStop( pProgress );
+        Extra_ProgressBarStop( pProgress );
     return pNtk;
 }
 
@@ -393,7 +393,7 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         if ( ResetValue != 0 && ResetValue != 1 && ResetValue != 2 )
         {
             p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
-            sprintf( p->sError, "The .latch line has an unknown reset value (%s).", vTokens->pArray[3] );
+            sprintf( p->sError, "The .latch line has an unknown reset value (%s).", (char*)vTokens->pArray[3] );
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
         }
@@ -445,7 +445,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
     nFanins = vTokens->nSize - 2;
     if ( nFanins == 0 )
     {
-        while ( vTokens = Io_ReadBlifGetTokens(p) )
+        while ( (vTokens = Io_ReadBlifGetTokens(p)) )
         {
             pToken = vTokens->pArray[0];
             if ( pToken[0] == '.' )
@@ -467,7 +467,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
     }
     else
     {
-        while ( vTokens = Io_ReadBlifGetTokens(p) )
+        while ( (vTokens = Io_ReadBlifGetTokens(p)) )
         {
             pToken = vTokens->pArray[0];
             if ( pToken[0] == '.' )
@@ -567,7 +567,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     if ( pGate == NULL )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
-        sprintf( p->sError, "Cannot find gate \"%s\" in the library.", vTokens->pArray[1] );
+        sprintf( p->sError, "Cannot find gate \"%s\" in the library.", (char*)vTokens->pArray[1] );
         Io_ReadBlifPrintErrorMessage( p );
         return 1;
     }
@@ -642,7 +642,7 @@ int Io_ReadBlifNetworkSubcircuit( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     // set the pointer to the node names
     Abc_ObjSetData( pBox, vNames );
     // remember the line of the file
-    pBox->pCopy = (void *)Extra_FileReaderGetLineNumber(p->pReader, 0);
+    pBox->pCopy = (void *)(PORT_PTRINT_T)Extra_FileReaderGetLineNumber(p->pReader, 0);
     return 0;
 }
 
@@ -697,7 +697,7 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     if ( pNet == NULL )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
-        sprintf( p->sError, "Cannot find object corresponding to %s on .input_arrival line.", vTokens->pArray[1] );
+        sprintf( p->sError, "Cannot find object corresponding to %s on .input_arrival line.", (char*)vTokens->pArray[1] );
         Io_ReadBlifPrintErrorMessage( p );
         return 1;
     }
@@ -706,7 +706,7 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     if ( *pFoo1 != '\0' || *pFoo2 != '\0' )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
-        sprintf( p->sError, "Bad value (%s %s) for rise or fall time on .input_arrival line.", vTokens->pArray[2], vTokens->pArray[3] );
+        sprintf( p->sError, "Bad value (%s %s) for rise or fall time on .input_arrival line.", (char*)vTokens->pArray[2], (char*)vTokens->pArray[3] );
         Io_ReadBlifPrintErrorMessage( p );
         return 1;
     }
@@ -745,7 +745,7 @@ int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vToken
     if ( *pFoo1 != '\0' || *pFoo2 != '\0' )
     {
         p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
-        sprintf( p->sError, "Bad value (%s %s) for rise or fall time on .default_input_arrival line.", vTokens->pArray[1], vTokens->pArray[2] );
+        sprintf( p->sError, "Bad value (%s %s) for rise or fall time on .default_input_arrival line.", (char*)vTokens->pArray[1], (char*)vTokens->pArray[2] );
         Io_ReadBlifPrintErrorMessage( p );
         return 1;
     }
@@ -914,15 +914,15 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
     Vec_Ptr_t * pNames;
     Abc_Ntk_t * pNtkModel;
     Abc_Obj_t * pObj, * pNet;
-    char * pName, * pActual;
-    int i, Length, Start;
+    char * pName = NULL, * pActual;
+    int i, Length, Start = -1;
 
     // get the model for this box
     pNames = pBox->pData;
     if ( !stmm_lookup( tName2Model, Vec_PtrEntry(pNames, 0), (char **)&pNtkModel ) )
     {
-        p->LineCur = (int)pBox->pCopy;
-        sprintf( p->sError, "Cannot find the model for subcircuit %s.", Vec_PtrEntry(pNames, 0) );
+        p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
+        sprintf( p->sError, "Cannot find the model for subcircuit %s.", (char*)Vec_PtrEntry(pNames, 0) );
         Io_ReadBlifPrintErrorMessage( p );
         return 1;
     }
@@ -939,7 +939,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
             pActual = Io_ReadBlifCleanName(pName);
             if ( pActual == NULL )
             {
-                p->LineCur = (int)pBox->pCopy;
+                p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
                 sprintf( p->sError, "Cannot parse formal/actual name pair \"%s\".", pName );
                 Io_ReadBlifPrintErrorMessage( p );
                 return 1;
@@ -950,8 +950,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
             pObj = Abc_NtkFindNet( pNtkModel, pName );
             if ( pObj == NULL )
             {
-                p->LineCur = (int)pBox->pCopy;
-                sprintf( p->sError, "Cannot find formal input \"%s\" as an PI of model \"%s\".", pName, Vec_PtrEntry(pNames, 0) );
+                p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
+                sprintf( p->sError, "Cannot find formal input \"%s\" as an PI of model \"%s\".", pName, (char*)Vec_PtrEntry(pNames, 0) );
                 Io_ReadBlifPrintErrorMessage( p );
                 return 1;
             }
@@ -967,7 +967,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
             // remember the actual name in the net
             if ( pObj->pCopy != NULL )
             {
-                p->LineCur = (int)pBox->pCopy;
+                p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
                 sprintf( p->sError, "Formal input \"%s\" is used more than once.", pName );
                 Io_ReadBlifPrintErrorMessage( p );
                 return 1;
@@ -987,8 +987,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pActual = (void *)pObj->pCopy;
         if ( pActual == NULL )
         {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Formal input \"%s\" of model %s is not driven.", pName, Vec_PtrEntry(pNames, 0) );
+            p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
+            sprintf( p->sError, "Formal input \"%s\" of model %s is not driven.", pName, (char*)Vec_PtrEntry(pNames, 0) );
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
         }
@@ -1006,7 +1006,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pActual = Io_ReadBlifCleanName(pName);
         if ( pActual == NULL )
         {
-            p->LineCur = (int)pBox->pCopy;
+            p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
             sprintf( p->sError, "Cannot parse formal/actual name pair \"%s\".", pName );
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
@@ -1017,8 +1017,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pObj = Abc_NtkFindNet( pNtkModel, pName );
         if ( pObj == NULL )
         {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Cannot find formal output \"%s\" as an PO of model \"%s\".", pName, Vec_PtrEntry(pNames, 0) );
+            p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
+            sprintf( p->sError, "Cannot find formal output \"%s\" as an PO of model \"%s\".", pName, (char*)Vec_PtrEntry(pNames, 0) );
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
         }
@@ -1026,7 +1026,7 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pObj = Abc_ObjFanout0(pObj);
         if ( pObj->pCopy != NULL )
         {
-            p->LineCur = (int)pBox->pCopy;
+            p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
             sprintf( p->sError, "Formal output \"%s\" is used more than once.", pName );
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
@@ -1039,8 +1039,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pActual = (void *)pObj->pCopy;
         if ( pActual == NULL )
         {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Formal output \"%s\" of model %s is not driven.", pName, Vec_PtrEntry(pNames, 0) );
+            p->LineCur = (int)(PORT_PTRINT_T)pBox->pCopy;
+            sprintf( p->sError, "Formal output \"%s\" of model %s is not driven.", pName, (char*)Vec_PtrEntry(pNames, 0) );
             Io_ReadBlifPrintErrorMessage( p );
             return 1;
         }
diff --git a/src/base/io/ioReadBlifAig.c b/src/base/io/ioReadBlifAig.c
index c448bab6..75552192 100644
--- a/src/base/io/ioReadBlifAig.c
+++ b/src/base/io/ioReadBlifAig.c
@@ -713,7 +713,7 @@ static int Io_BlifParseLatch( Io_BlifMan_t * p, char * pLine )
         Init = 2;
     if ( Init < 0 || Init > 2 )
     {
-        sprintf( p->sError, "Line %d: Initial state of the latch is incorrect (%s).", Io_BlifGetLine(p, pToken), Vec_PtrEntry(p->vTokens,3) );
+        sprintf( p->sError, "Line %d: Initial state of the latch is incorrect (%s).", Io_BlifGetLine(p, pToken), (char*)Vec_PtrEntry(p->vTokens,3) );
         return 0;
     }
     if ( Init == 0 )
@@ -731,12 +731,12 @@ static int Io_BlifParseLatch( Io_BlifMan_t * p, char * pLine )
     pObj = Io_BlifHashFindOrAdd( p, Vec_PtrEntry(p->vTokens,2) );
     if ( pObj->fPi )
     {
-        sprintf( p->sError, "Line %d: Primary input (%s) is also defined latch output.", Io_BlifGetLine(p, pToken), Vec_PtrEntry(p->vTokens,2) );
+        sprintf( p->sError, "Line %d: Primary input (%s) is also defined latch output.", Io_BlifGetLine(p, pToken), (char*)Vec_PtrEntry(p->vTokens,2) );
         return 0;
     }
     if ( pObj->fLo )
     {
-        sprintf( p->sError, "Line %d: Latch output (%s) is defined as the output of another latch.", Io_BlifGetLine(p, pToken), Vec_PtrEntry(p->vTokens,2) );
+        sprintf( p->sError, "Line %d: Latch output (%s) is defined as the output of another latch.", Io_BlifGetLine(p, pToken), (char*)Vec_PtrEntry(p->vTokens,2) );
         return 0;
     }
     pObj->fLo = 1;
@@ -970,7 +970,7 @@ static int Io_BlifParseConstruct( Io_BlifMan_t * p )
         
         // add the latch box
         pLatch = Abc_NtkCreateLatch( pAig );
-        pLatch->pData = (void *)pObjIo->Init;
+        pLatch->pData = (void *)(PORT_PTRUINT_T)pObjIo->Init;
         Abc_ObjAssignName( pLatch, pObjIo->pName, "L" );
         Abc_ObjAddFanin( pLatch, pObj  );
 
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index b5fb632f..52d7eb06 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -768,7 +768,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
             Abc_Obj_t * pObj;
             // set register numbers
             Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
-                pObj->pNext = (Abc_Obj_t *)k;
+                pObj->pNext = (Abc_Obj_t *)(PORT_PTRINT_T)k;
             // derive register
             pMod->pNtk->vOnehots = Vec_PtrAlloc( Vec_PtrSize(pMod->vOnehots) );
             Vec_PtrForEachEntry( pMod->vOnehots, pLine, k )
@@ -932,7 +932,7 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine )
                 Init = 2;
             if ( Init < 0 || Init > 2 )
             {
-                sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
+                sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Io_MvGetLine(p->pMan, pToken), (char*)Vec_PtrEntry(vTokens,3) );
                 return 0;
             }
             if ( Init == 0 )
@@ -1099,9 +1099,9 @@ static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine )
         }
         // save register name
 //        Vec_PtrPush( vResult, Abc_ObjName(pNet) );
-        Vec_IntPush( vResult, (int)Abc_ObjFanin0(pTerm)->pNext );
+        Vec_IntPush( vResult, (int)(PORT_PTRINT_T)Abc_ObjFanin0(pTerm)->pNext );
 //        printf( "%d(%d) ", (int)Abc_ObjFanin0(pTerm)->pNext, ((int)Abc_ObjFanin0(pTerm)->pData) -1 );
-        printf( "%d", ((int)Abc_ObjFanin0(pTerm)->pData)-1 );
+        printf( "%d", ((int)(PORT_PTRINT_T)Abc_ObjFanin0(pTerm)->pData)-1 );
     }
     printf( "\n" );
     return vResult;
@@ -1123,7 +1123,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     Abc_Obj_t * pObj;
-    Io_MvVar_t * pVar;
+    Io_MvVar_t * pVar = NULL;
     Extra_MmFlex_t * pFlex;
     char * pName;
     int nCommas, nValues, i, k;
@@ -1135,7 +1135,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
     // get the number of values
     if ( Vec_PtrSize(vTokens) <= nCommas + 2 )
     {
-        sprintf( p->pMan->sError, "Line %d: The number of values in not specified in .mv line.", Io_MvGetLine(p->pMan, pName), pName );
+        sprintf( p->pMan->sError, "Line %d: The number of values in not specified in .mv line.", Io_MvGetLine(p->pMan, pName) );
         return 0;
     }
     nValues = atoi( Vec_PtrEntry(vTokens,nCommas+2) );
@@ -1178,6 +1178,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
         Abc_ObjSetMvVar( pObj, pVar );
     }
     // make sure the names are unique
+    assert(pVar);
     if ( pVar->pNames )
     {
         for ( i = 0; i < nValues; i++ )
@@ -1398,7 +1399,7 @@ static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
     if ( p->pMan->fBlifMv )
     {
 //        Vec_Att_t * p = Abc_NtkMvVar( pNtk );
-        int nValues = Abc_ObjMvVarNum(pOutNet);
+//        int nValues = Abc_ObjMvVarNum(pOutNet);
 //        sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
         sprintf( Buffer, "1 - - =1\n0 - - =2\n" );
         pNode->pData = Abc_SopRegister( p->pNtk->pManFunc, Buffer );
@@ -1776,7 +1777,7 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
     pGate = Mio_LibraryReadGateByName( pGenlib, vTokens->pArray[1] );
     if ( pGate == NULL )
     {
-        sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), vTokens->pArray[1] );
+        sprintf( p->pMan->sError, "Line %d: Cannot find gate \"%s\" in the library.", Io_MvGetLine(p->pMan, pName), (char*)vTokens->pArray[1] );
         return 0;
     }
 
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index bea9bf69..2f97644a 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -212,7 +212,7 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
             Abc_ObjSetData( pObj, Abc_SopCreateBuf(pNtk->pManFunc) );
         else
         {
-            printf( "%s: Unknown gate type \"%s\".\n", Extra_FileReaderGetFileName(p), pObj->pData );
+            printf( "%s: Unknown gate type \"%s\".\n", Extra_FileReaderGetFileName(p), (char*)pObj->pData );
             Abc_NtkDelete( pNtk );
             return NULL;
         }
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
index 6a1360d0..ad35c73b 100644
--- a/src/base/io/ioReadEqn.c
+++ b/src/base/io/ioReadEqn.c
@@ -100,7 +100,7 @@ Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
     // go through the lines of the file
     vVars  = Vec_PtrAlloc( 100 );
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
-    for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+    for ( iLine = 0; (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
     {
         Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
 
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index cbee81ef..4b326783 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -83,7 +83,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
     Vec_Ptr_t * vTokens;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pTermPi, * pTermPo, * pNode;
-    Vec_Str_t ** ppSops;
+    Vec_Str_t ** ppSops = NULL;
     char Buffer[100];
     int nInputs = -1, nOutputs = -1, nProducts = -1;
     char * pCubeIn, * pCubeOut;
@@ -95,7 +95,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
     // go through the lines of the file
     nCubes = 0;
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
-    for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+    for ( iLine = 0; (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
     {
         Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
 
@@ -193,14 +193,14 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
             pCubeOut = vTokens->pArray[1];
             if ( strlen(pCubeIn) != (unsigned)nInputs )
             {
-                printf( "%s (line %d): Input cube length (%d) differs from the number of inputs (%d).\n", 
+                printf( "%s (line %d): Input cube length (%zu) differs from the number of inputs (%d).\n",
                     Extra_FileReaderGetFileName(p), iLine+1, strlen(pCubeIn), nInputs );
                 Abc_NtkDelete( pNtk );
                 return NULL;
             }
             if ( strlen(pCubeOut) != (unsigned)nOutputs )
             {
-                printf( "%s (line %d): Output cube length (%d) differs from the number of outputs (%d).\n", 
+                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 );
                 return NULL;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index a5d32e39..119b4d75 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -101,7 +101,7 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
     if ( pFile == NULL )
     {
         fprintf( stdout, "Cannot open input file \"%s\". ", pFileName );
-        if ( pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
+        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", ".bench", ".pla", ".baf", ".aig" )) )
             fprintf( stdout, "Did you mean \"%s\"?", pFileName );
         fprintf( stdout, "\n" );
        return NULL;
@@ -715,7 +715,7 @@ FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mo
     }
     else
     {
-        if ( c = Abc_FrameReadFlag( (char*)PathVar ) )
+        if ( (c = Abc_FrameReadFlag( (char*)PathVar )) )
         {
             char ActualFileName[4096];
             FILE * fp = 0;
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 9e5ee8b4..45e1e965 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -19,10 +19,13 @@
 
 ***********************************************************************/
 
+// The code in this file is developed in collaboration with Mark Jarvin of Toronto.
+
 #include "ioAbc.h"
 
-#include <bzlib.h>
 #include <stdarg.h>
+#include "bzlib.h"
+#include "zlib.h"
 
 #ifdef _WIN32
 #define vsnprintf _vsnprintf
@@ -132,9 +135,9 @@ Binary Format Definition
 
 */
 
-static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;    }
-static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj )                   { return (unsigned)pObj->pCopy;  }
-static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCopy = (void *)Num;     }
+static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;                   }
+static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj )                   { return (unsigned)(PORT_PTRINT_T)pObj->pCopy;  }
+static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCopy = (void *)(PORT_PTRINT_T)Num;     }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -152,7 +155,7 @@ static void     Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num )  { pObj->pCo
   SeeAlso     []
 
 ***********************************************************************/
-int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x )
+int Io_WriteAigerEncode( unsigned char * pBuffer, int Pos, unsigned x )
 {
     unsigned char ch;
     while (x & ~0x7f)
@@ -215,13 +218,13 @@ Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits )
     int Pos = 0, Lit, LitPrev, Diff, i;
     vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) );
     LitPrev = Vec_IntEntry( vLits, 0 );
-    Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev ); 
+    Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, LitPrev ); 
     Vec_IntForEachEntryStart( vLits, Lit, i, 1 )
     {
         Diff = Lit - LitPrev;
         Diff = (Lit < LitPrev)? -Diff : Diff;
         Diff = (Diff << 1) | (int)(Lit < LitPrev);
-        Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff );
+        Pos = Io_WriteAigerEncode( (unsigned char *)Vec_StrArray(vBinary), Pos, Diff );
         LitPrev = Lit;
         if ( Pos + 10 > vBinary->nCap )
             Vec_StrGrow( vBinary, vBinary->nCap+1 );
@@ -260,7 +263,7 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i
     ProgressBar * pProgress;
     FILE * pFile;
     Abc_Obj_t * pObj, * pDriver;
-    int i, nNodes, Pos, nBufferSize;
+    int i, nNodes, nBufferSize, Pos;
     unsigned char * pBuffer;
     unsigned uLit0, uLit1, uLit;
 
@@ -376,6 +379,126 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i
     fclose( pFile );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
+{
+    ProgressBar * pProgress;
+    gzFile pFile;
+    Abc_Obj_t * pObj, * pDriver;
+    int i, nNodes, Pos, nBufferSize;
+    unsigned char * pBuffer;
+    unsigned uLit0, uLit1, uLit;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the output stream
+    pFile = gzopen( pFileName, "wb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteAigerGz(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( !Abc_LatchIsInit0(pObj) )
+        {
+            fprintf( stdout, "Io_WriteAigerGz(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" );
+            return;
+        }
+
+    // set the node numbers to be used in the output file
+    nNodes = 0;
+    Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Io_ObjSetAigerNum( pObj, nNodes++ );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        Io_ObjSetAigerNum( pObj, nNodes++ );
+
+    // write the header "M I L O A" where M = I + L + A
+    gzprintf( pFile, "aig %u %u %u %u %u\n", 
+              Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
+              Abc_NtkPiNum(pNtk),
+              Abc_NtkLatchNum(pNtk),
+              Abc_NtkPoNum(pNtk),
+              Abc_NtkNodeNum(pNtk) );
+
+    // if the driver node is a constant, we need to complement the literal below
+    // because, in the AIGER format, literal 0/1 is represented as number 0/1
+    // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
+
+    // write latch drivers
+    Abc_NtkForEachLatchInput( pNtk, pObj, i )
+    {
+        pDriver = Abc_ObjFanin0(pObj);
+        gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+    }
+
+    // write PO drivers
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        pDriver = Abc_ObjFanin0(pObj);
+        gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
+    }
+
+    // write the nodes into the buffer
+    Pos = 0;
+    nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge
+    pBuffer = ALLOC( char, nBufferSize );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        uLit  = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 );
+        uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) );
+        uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) );
+        assert( uLit0 < uLit1 );
+        Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit  - uLit1 );
+        Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
+        if ( Pos > nBufferSize - 10 )
+        {
+            printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
+            gzclose( pFile );
+            return;
+        }
+    }
+    assert( Pos < nBufferSize );
+    Extra_ProgressBarStop( pProgress );
+
+    // write the buffer
+    gzwrite(pFile, pBuffer, Pos);
+    free( pBuffer );
+
+    // write the symbol table
+    if ( fWriteSymbols )
+    {
+        // write PIs
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            gzprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
+        // write latches
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            gzprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) );
+        // write POs
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            gzprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) );
+    }
+
+    // write the comment
+    gzprintf( pFile, "c\n" );
+    if ( pNtk->pName && strlen(pNtk->pName) > 0 )
+        gzprintf( pFile, ".model %s\n", pNtk->pName );
+    gzprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
+    gzprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
+    gzclose( pFile );
+}
+
  
 /**Function*************************************************************
 
@@ -448,7 +571,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
     ProgressBar * pProgress;
 //    FILE * pFile;
     Abc_Obj_t * pObj, * pDriver;
-    int i, nNodes, Pos, nBufferSize, bzError;
+    int i, nNodes, nBufferSize, bzError, Pos;
     unsigned char * pBuffer;
     unsigned uLit0, uLit1, uLit;
     bz2file b;
@@ -462,6 +585,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
             return;
         }
 
+    // write the GZ file
+    if (!strncmp(pFileName+strlen(pFileName)-3,".gz",3)) 
+    {
+        Io_WriteAigerGz( pNtk, pFileName, fWriteSymbols );
+        return;
+    }
+
     memset(&b,0,sizeof(b));
     b.nBytesMax = (1<<12);
     b.buf = ALLOC( char,b.nBytesMax );
diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c
index 33487041..6a9af2f2 100644
--- a/src/base/io/ioWriteBaf.c
+++ b/src/base/io/ioWriteBaf.c
@@ -126,29 +126,29 @@ void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName )
     Abc_NtkCleanCopy( pNtk );
     nNodes = 1;
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pCopy = (void *)nNodes++;
+        pObj->pCopy = (void *)(PORT_PTRINT_T)nNodes++;
     Abc_AigForEachAnd( pNtk, pObj, i )
-        pObj->pCopy = (void *)nNodes++;
+        pObj->pCopy = (void *)(PORT_PTRINT_T)nNodes++;
 
     // write the nodes into the buffer
     nAnds = 0;
     nBufferSize = Abc_NtkNodeNum(pNtk) * 2 + Abc_NtkCoNum(pNtk);
-    pBufferNode = ALLOC( int, nBufferSize );
+    pBufferNode = ALLOC( unsigned, nBufferSize );
     pProgress = Extra_ProgressBarStart( stdout, nBufferSize );
     Abc_AigForEachAnd( pNtk, pObj, i )
     {
         Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
-        pBufferNode[nAnds++] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
-        pBufferNode[nAnds++] = (((int)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj);
+        pBufferNode[nAnds++] = (((int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
+        pBufferNode[nAnds++] = (((int)(PORT_PTRINT_T)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj);
     }
 
     // write the COs into the buffer
     Abc_NtkForEachCo( pNtk, pObj, i )
     {
         Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
-        pBufferNode[nAnds] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
+        pBufferNode[nAnds] = (((int)(PORT_PTRINT_T)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
         if ( Abc_ObjFanoutNum(pObj) > 0 && Abc_ObjIsLatch(Abc_ObjFanout0(pObj)) )
-            pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((unsigned)Abc_ObjData(Abc_ObjFanout0(pObj)) & 3);
+            pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((int)(PORT_PTRINT_T)Abc_ObjData(Abc_ObjFanout0(pObj)) & 3);
         nAnds++;
     }
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index a0105a6b..342dc0aa 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -434,7 +434,7 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
     int Reset;
     pNetLi = Abc_ObjFanin0( Abc_ObjFanin0(pLatch) );
     pNetLo = Abc_ObjFanout0( Abc_ObjFanout0(pLatch) );
-    Reset  = (int)Abc_ObjData( pLatch );
+    Reset  = (int)(PORT_PTRUINT_T)Abc_ObjData( pLatch );
     // write the latch line
     fprintf( pFile, ".latch" );
     fprintf( pFile, " %10s",    Abc_ObjName(pNetLi) );
@@ -470,7 +470,7 @@ void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode, int Length )
         Io_NtkWriteNodeFanins( pFile, pNode );
         fprintf( pFile, "\n" );
         // write the cubes
-        fprintf( pFile, "%s", Abc_ObjData(pNode) );
+        fprintf( pFile, "%s", (char*)Abc_ObjData(pNode) );
     }
 }
 
diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c
index 86891fee..266ee95f 100644
--- a/src/base/io/ioWriteBlifMv.c
+++ b/src/base/io/ioWriteBlifMv.c
@@ -341,7 +341,7 @@ void Io_NtkWriteBlifMvLatch( FILE * pFile, Abc_Obj_t * pLatch )
     int Reset;
     pNetLi = Abc_ObjFanin0( Abc_ObjFanin0(pLatch) );
     pNetLo = Abc_ObjFanout0( Abc_ObjFanout0(pLatch) );
-    Reset  = (int)Abc_ObjData( pLatch );
+    Reset  = (int)(PORT_PTRUINT_T)Abc_ObjData( pLatch );
     // write the latch line
     fprintf( pFile, ".latch" );
     fprintf( pFile, " %10s",    Abc_ObjName(pNetLi) );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index b8ca6f67..88028105 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -95,7 +95,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     }
 
     // transform logic functions from BDD to SOP
-    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+    if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
         {
@@ -430,7 +430,7 @@ void Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     }
 
     // transform logic functions from BDD to SOP
-    if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
+    if ( (fHasBdds = Abc_NtkIsBddLogic(pNtk)) )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
         {
diff --git a/src/base/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c
index 94c6e032..228e4ae9 100644
--- a/src/base/io/ioWriteEqn.c
+++ b/src/base/io/ioWriteEqn.c
@@ -212,7 +212,7 @@ void Io_NtkWriteEqnCos( FILE * pFile, Abc_Ntk_t * pNtk )
 int Io_NtkWriteEqnCheck( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
-    char * pName;
+    char * pName = NULL;
     int i, k, Length;
     int RetValue = 1;
 
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 4b316416..653e2f74 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -126,7 +126,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
 
     // mark the CI nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)i;
+        pNode->pCopy = (Abc_Obj_t *)(PORT_PTRUINT_T)i;
 
     // write the cubes
     pProgress = Extra_ProgressBarStart( stdout, nOutputs );
@@ -142,9 +142,9 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
         if ( !Abc_ObjIsNode(pDriver) )
         {
             assert( Abc_ObjIsCi(pDriver) );
-            pCubeIn[(int)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode);
+            pCubeIn[(int)(PORT_PTRUINT_T)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode);
             fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
-            pCubeIn[(int)pDriver->pCopy] = '-';
+            pCubeIn[(int)(PORT_PTRUINT_T)pDriver->pCopy] = '-';
             continue;
         }
         if ( Abc_NodeIsConst(pDriver) )
@@ -164,8 +164,8 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
             Abc_ObjForEachFanin( pDriver, pFanin, k )
             {
                 pFanin = Abc_ObjFanin0Ntk(pFanin);
-                assert( (int)pFanin->pCopy < nInputs );
-                pCubeIn[(int)pFanin->pCopy] = pCube[k];
+                assert( (int)(PORT_PTRUINT_T)pFanin->pCopy < nInputs );
+                pCubeIn[(int)(PORT_PTRUINT_T)pFanin->pCopy] = pCube[k];
             }
             fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
         }
@@ -174,7 +174,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
         {
             pFanin = Abc_ObjFanin0Ntk(pFanin);
             assert( Abc_ObjIsCi(pFanin) );
-            pCubeIn[(int)pFanin->pCopy] = '-';
+            pCubeIn[(int)(PORT_PTRUINT_T)pFanin->pCopy] = '-';
         }
         Extra_ProgressBarUpdate( pProgress, i, NULL );
     }
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index c704c6a1..41932dca 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -458,7 +458,7 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     if ( i == Abc_NtkLatchNum(pNtk) )
         return;
     // write the initial values
-    fprintf( pFile, "  initial begin\n", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0)))) );
+    fprintf( pFile, "  initial begin\n" );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index 1f090cf4..d69055a4 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -22,6 +22,7 @@
 
 #ifndef _WIN32
 #include <readline/readline.h>
+#include <readline/history.h>
 #endif
 
 ////////////////////////////////////////////////////////////////////////
@@ -64,14 +65,17 @@ char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc )
 ***********************************************************************/
 char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc )
 {
-    static char Buffer[1000], Prompt[1000];
+    static char Prompt[1000];
+#ifndef _WIN32
+    static char * line = NULL;
+#endif
+
     sprintf( Prompt, "abc %02d> ", pAbc->nSteps );
 #ifdef _WIN32
     fprintf( pAbc->Out, "%s", Prompt );
-    fgets( Buffer, 999, stdin );
-    return Buffer;
+    fgets( Prompt, 999, stdin );
+    return Prompt;
 #else
-    static char* line = NULL;
     if (line != NULL) free(line);
     line = readline(Prompt);  
     if (line == NULL){ printf("***EOF***\n"); exit(0); }
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index 322ce720..93fc7b5d 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -293,7 +293,7 @@ Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName )
 {
     Abc_Ntk_t * pNtkNew;
     // check if the network exists
-    if ( pNtkNew = Abc_LibFindModelByName( pMan->pDesign, pName ) )
+    if ( (pNtkNew = Abc_LibFindModelByName( pMan->pDesign, pName )) )
         return pNtkNew;
 //printf( "Creating network %s.\n", pName );
     // create new network
@@ -319,7 +319,7 @@ Abc_Ntk_t * Ver_ParseFindOrCreateNetwork( Ver_Man_t * pMan, char * pName )
 Abc_Obj_t * Ver_ParseFindNet( Abc_Ntk_t * pNtk, char * pName )
 {
     Abc_Obj_t * pObj;
-    if ( pObj = Abc_NtkFindNet(pNtk, pName) )
+    if ( (pObj = Abc_NtkFindNet(pNtk, pName)) )
         return pObj;
     if ( !strcmp( pName, "1\'b0" ) || !strcmp( pName, "1\'bx" ) )
         return Abc_NtkFindOrCreateNet( pNtk, "1\'b0" );
@@ -583,7 +583,7 @@ int Ver_ParseInsertsSuffix( Ver_Man_t * pMan, char * pWord, int nMsb, int nLsb )
     assert( nMsb >= 0 && nMsb < 128 );
     assert( nLsb >= 0 && nLsb < 128 );
     Value = (nMsb << 8) | nLsb;
-    st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)Value );
+    st_insert( pMan->tName2Suffix, Extra_UtilStrsav(pWord), (char *)(PORT_PTRUINT_T)Value );
     return 1;
 }
 
@@ -764,7 +764,7 @@ int Ver_ParseConstant( Ver_Man_t * pMan, char * pWord )
       if ( pWord[i] == 'x' ) 
           Vec_PtrPush( pMan->vNames, (void *)0 );
       else 
-          Vec_PtrPush( pMan->vNames, (void *)(pWord[i]-'0') );
+          Vec_PtrPush( pMan->vNames, (void *)(PORT_PTRUINT_T)(pWord[i]-'0') );
     }
     return 1;
 }
@@ -1211,7 +1211,7 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
                         Ver_ParsePrintErrorMessage( pMan );
                         return 0;
                     }
-                    Vec_PtrPush( pMan->vNames, (void *)strlen(pEquation) );
+                    Vec_PtrPush( pMan->vNames, (void *)(PORT_PTRUINT_T)strlen(pEquation) );
                     Vec_PtrPush( pMan->vNames, pEquation );
                     // get the buffer
                     pFunc = (Hop_Obj_t *)Mio_LibraryReadBuf(Abc_FrameReadLibGen());
@@ -1248,7 +1248,7 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk )
             for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
             {
                 // get the name of this signal
-                Length = (int)Vec_PtrEntry( pMan->vNames, 2*i );
+                Length = (int)(PORT_PTRUINT_T)Vec_PtrEntry( pMan->vNames, 2*i );
                 pName  = Vec_PtrEntry( pMan->vNames, 2*i + 1 );
                 pName[Length] = 0;
                 // find the corresponding net
@@ -2371,7 +2371,6 @@ int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs )
                 if ( pBundle )
                 Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
                 {
-                    char * pName = Abc_ObjName(pNet);
                     if ( Abc_ObjFaninNum(pNet) == 0 ) // non-driven
                         if ( strcmp(Abc_ObjName(pNet), "1\'b0") && strcmp(Abc_ObjName(pNet), "1\'b1") ) // diff from a const
                             return 1;
@@ -2392,7 +2391,7 @@ int Ver_ParseCheckNondrivenNets( Vec_Ptr_t * vUndefs )
 ***********************************************************************/
 int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
 {
-    Ver_Bundle_t * pBundle;
+    Ver_Bundle_t * pBundle = NULL;
     Abc_Obj_t * pBox, * pNet;
     int k, j, m;
     // go through instances of this type
@@ -2406,6 +2405,7 @@ int Ver_ParseFormalNetsAreDriven( Abc_Ntk_t * pNtk, char * pNameFormal )
         if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
             continue;
         // check if all nets are driven in this bundle
+        assert(pBundle); // Verify that pBundle was assigned to.
         Vec_PtrForEachEntry( pBundle->vNetsActual, pNet, m )
             if ( Abc_ObjFaninNum(pNet) > 0 )
                 return 1;
@@ -2461,7 +2461,7 @@ int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBu
 {
     char Buffer[200];
     char * pName;
-    Ver_Bundle_t * pBundle;
+    Ver_Bundle_t * pBundle = NULL;
     Abc_Obj_t * pBox, * pTerm, * pTermNew, * pNetAct, * pNetFormal;
     int k, j, m;
 
@@ -2496,6 +2496,7 @@ int Ver_ParseDriveFormal( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_Bundle_t * pBu
         if ( j == Vec_PtrSize((Vec_Ptr_t *)pBox->pCopy) )
             continue;
         // check if any nets are driven in this bundle
+        assert(pBundle); // Verify pBundle was assigned to.
         Vec_PtrForEachEntry( pBundle->vNetsActual, pNetAct, m )
             if ( Abc_ObjFaninNum(pNetAct) > 0 )
             {
@@ -2705,7 +2706,7 @@ void Ver_ParsePrintLog( Ver_Man_t * pMan )
     {
         Vec_Ptr_t * vBundles;
         Ver_Bundle_t * pBundle;
-        int j, nActNets, Counter = 0, CounterBoxes = 0;
+        int j, nActNets, Counter = 0;
         // count the number of instances with dangling outputs
         Vec_PtrForEachEntry( pMan->pDesign->vModules, pNtk, i )
         {
@@ -2784,7 +2785,7 @@ void Ver_ParsePrintLog( Ver_Man_t * pMan )
 ***********************************************************************/
 int Ver_ParseAttachBoxes( Ver_Man_t * pMan )
 {
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk = NULL;
     Ver_Bundle_t * pBundle;
     Vec_Ptr_t * vUndefs;
     int i, RetValue, Counter, nMaxBoxSize;
@@ -2813,7 +2814,7 @@ int Ver_ParseAttachBoxes( Ver_Man_t * pMan )
         // go through undef box types
         pBundle = NULL;
         Vec_PtrForEachEntry( vUndefs, pNtk, i )
-            if ( pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter ) )
+            if ( (pBundle = Ver_ParseGetNondrivenBundle( pNtk, Counter )) )
                 break;
         if ( pBundle == NULL )
         {
diff --git a/src/base/ver/verFormula.c b/src/base/ver/verFormula.c
index 19a2c523..e9588ba9 100644
--- a/src/base/ver/verFormula.c
+++ b/src/base/ver/verFormula.c
@@ -237,7 +237,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
             v = Ver_FormulaParserFindVar( pTemp, vNames );
             if ( *pTemp == '\\' )
                 pTemp++;
-            pTemp += (int)Vec_PtrEntry( vNames, 2*v ) - 1;
+            pTemp += (int)(PORT_PTRUINT_T)Vec_PtrEntry( vNames, 2*v ) - 1;
 
             // assume operation AND, if vars follow one another
             if ( Flag == VER_PARSE_FLAG_VAR )
@@ -404,7 +404,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
     nLength = pTemp - pString;
     for ( i = 0; i < Vec_PtrSize(vNames)/2; i++ )
     {
-        nLength2 = (int)Vec_PtrEntry( vNames, 2*i + 0 );
+        nLength2 = (int)(PORT_PTRUINT_T)Vec_PtrEntry( vNames, 2*i + 0 );
         if ( nLength2 != nLength )
             continue;
         pTemp2   = Vec_PtrEntry( vNames, 2*i + 1 );
@@ -413,7 +413,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
         return i;
     }
     // could not find - add and return the number
-    Vec_PtrPush( vNames, (void *)nLength );
+    Vec_PtrPush( vNames, (void *)(PORT_PTRUINT_T)nLength );
     Vec_PtrPush( vNames, pString );
     return i;
 }
@@ -431,7 +431,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
 ***********************************************************************/
 void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
 {
-    Hop_Obj_t * pRes;
+    Hop_Obj_t * pRes = NULL;
     int v, fCompl;
     char Symbol;
 
@@ -453,7 +453,7 @@ void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, c
     while ( *pFormula != '}' )
     {
         v = Ver_FormulaParserFindVar( pFormula, vNames );
-        pFormula += (int)Vec_PtrEntry( vNames, 2*v );
+        pFormula += (int)(PORT_PTRUINT_T)Vec_PtrEntry( vNames, 2*v );
         while ( *pFormula == ' ' || *pFormula == ',' )
             pFormula++;
     }
author	Alan Mishchenko <alanmi@berkeley.edu>	2008-07-02 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2008-07-02 08:01:00 -0700
commit	303baf27cf34c2a57db97c4c567fd744241fa14b (patch)
tree	d6235cca48e7bdfe5884e517058c7791e66bb806 /src/base
parent	fa67e3c19e27c011517b91182eb3929412aaf402 (diff)
download	abc-303baf27cf34c2a57db97c4c567fd744241fa14b.tar.gz abc-303baf27cf34c2a57db97c4c567fd744241fa14b.tar.bz2 abc-303baf27cf34c2a57db97c4c567fd744241fa14b.zip