Version abc80702

19 files changed, 333 insertions, 96 deletions

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 )