Adding switch &w -n to modify the comment section of the AIGER file written.

42 files changed, 83 insertions, 79 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fcf6fd28..d6375312 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1191,7 +1191,7 @@ static inline int         Gia_ObjCellId( Gia_Man_t * p, int iLit )          { re
 extern int                 Gia_FileSize( char * pFileName );
 extern Gia_Man_t *         Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck );
 extern Gia_Man_t *         Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck );
-extern void                Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
+extern void                Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine );
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
 extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p );
 extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index cf185c33..03929aff 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1076,10 +1076,9 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact )
+void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine )
 {
     int fVerbose = XAIG_VERBOSE;
-    int fWriteNewLine = 0;
     FILE * pFile;
     Gia_Man_t * p;
     Gia_Obj_t * pObj;
@@ -1438,7 +1437,7 @@ void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNu
 {
     char Buffer[100];
     sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
-    Gia_AigerWrite( p, Buffer, 0, 0 );
+    Gia_AigerWrite( p, Buffer, 0, 0, 0 );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 84d9f1b1..20987687 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1994,14 +1994,14 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
             }
         }
         // write equivalence classes
-        Gia_AigerWrite( pGia, "gore.aig", 0, 0 );
+        Gia_AigerWrite( pGia, "gore.aig", 0, 0, 0 );
         // reduce the model
         pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
             Gia_ManStop( pAux );
-            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
+            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0, 0 );
 //            Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
 //          Gia_ManPrintStatsShort( pReduce );
             Gia_ManStop( pReduce );
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c
index a055b5bc..50cb8ea7 100644
--- a/src/aig/gia/giaFalse.c
+++ b/src/aig/gia/giaFalse.c
@@ -457,7 +457,7 @@ Gia_Man_t * Gia_ManCheckOne( Gia_Man_t * p, int iOut, int iObj, int nTimeOut, in
     if ( pNew )
     {
         Gia_Man_t * pTemp = Gia_ManDupDfsNode( p, Gia_ManObj(p, iObj) );
-        Gia_AigerWrite( pTemp, "false.aig", 0, 0 );
+        Gia_AigerWrite( pTemp, "false.aig", 0, 0, 0 );
         Abc_Print( 1, "Dumping cone with %d nodes into file \"%s\".\n", Gia_ManAndNum(pTemp), "false.aig" );
         Gia_ManStop( pTemp );
     }
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 5d3e28f5..8e8461e1 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -626,7 +626,7 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis,
         Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
             Gia_ManStop( pGia );
 
-        Gia_AigerWrite( pMiter, "m3.aig", 0, 0 );
+        Gia_AigerWrite( pMiter, "m3.aig", 0, 0, 0 );
     }
     else 
     {
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index 0e040b6c..76419e93 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -1293,7 +1293,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
     // create AIG with two primary outputs (original and permuted)
     pPerm = Gia_ManDupPerm( p, vPiPerm );
     pDouble = Gia_ManDupAppendNew( p, pPerm );
-//Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
+//Gia_AigerWrite( pDouble, "test.aig", 0, 0, 0 );
 
     // analyze the two-output miter
     pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0, 0 );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 53b686a4..25355fe3 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -241,10 +241,10 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p )
     {
         Gia_Man_t * pTemp;
         pTemp = Gia_ManDupFlopClass( p, 1 );
-        Gia_AigerWrite( pTemp, "dom1.aig", 0, 0 );
+        Gia_AigerWrite( pTemp, "dom1.aig", 0, 0, 0 );
         Gia_ManStop( pTemp );
         pTemp = Gia_ManDupFlopClass( p, 2 );
-        Gia_AigerWrite( pTemp, "dom2.aig", 0, 0 );
+        Gia_AigerWrite( pTemp, "dom2.aig", 0, 0, 0 );
         Gia_ManStop( pTemp );
     }
 }
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index f04452ab..78d99ca8 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -573,7 +573,7 @@ int * Abc_FrameReadMiniLutNameMapping( Abc_Frame_t * pAbc )
     if ( pAbc->pGiaMiniAig == NULL || pAbc->pGiaMiniLut == NULL )
         return NULL;
     pGia = Gia_ManDup2( pAbc->pGiaMiniAig, pAbc->pGiaMiniLut );
-    //Gia_AigerWrite( pGia, "aig_m_lut.aig", 0, 0 );
+    //Gia_AigerWrite( pGia, "aig_m_lut.aig", 0, 0, 0 );
     // compute equivalences in this AIG
     pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose );
     Gia_ManStop( pTemp );
@@ -783,12 +783,12 @@ void Gia_MiniAigVerify( Abc_Frame_t * pAbc, char * pFileName )
     pEquivs = Abc_FrameReadMiniAigEquivClasses( pAbc );
     // dump miter for verification
     pGia = Gia_MiniAigMiter( p, pEquivs );
-    Gia_AigerWrite( pGia, pFileMiter, 0, 0 );
+    Gia_AigerWrite( pGia, pFileMiter, 0, 0, 0 );
     printf( "Dumped miter AIG in file \"%s\".\n", pFileMiter );
     Gia_ManStop( pGia );
     // dump reduced AIG
     pGia = Gia_MiniAigReduce( p, pEquivs );
-    Gia_AigerWrite( pGia, pFileReduced, 0, 0 );
+    Gia_AigerWrite( pGia, pFileReduced, 0, 0, 0 );
     printf( "Dumped reduced AIG in file \"%s\".\n", pFileReduced );
     Gia_ManStop( pGia );
     // cleanup
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index c1ce596d..de3f4049 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -439,7 +439,7 @@ void Gia_SweeperLogicDump( Gia_Man_t * p, Vec_Int_t * vProbeIds, int fDumpConds,
         Gia_ManStop( pGiaCond );
         printf( " and conditions" );
     }
-    Gia_AigerWrite( pGiaOuts, pFileName, 0, 0 );
+    Gia_AigerWrite( pGiaOuts, pFileName, 0, 0, 0 );
     Gia_ManStop( pGiaOuts );
     printf( " into file \"%s\".\n", pFileName );
 }
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 22212793..e136f68f 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -962,8 +962,8 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
         char * pNameGeneric = Extra_FileNameGeneric( pFileSpec ? pFileSpec : pGia->pSpec );
         sprintf( pFileName0, "%s_spec.aig", pNameGeneric );
         sprintf( pFileName1, "%s_impl.aig", pNameGeneric );
-        Gia_AigerWrite( pGia0, pFileName0, 0, 0 );
-        Gia_AigerWrite( pGia1, pFileName1, 0, 0 );
+        Gia_AigerWrite( pGia0, pFileName0, 0, 0, 0 );
+        Gia_AigerWrite( pGia1, pFileName1, 0, 0, 0 );
         ABC_FREE( pNameGeneric );
         printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 753bf2ae..3a3ccac6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10727,7 +10727,7 @@ int Abc_CommandExpand( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_NtkDelete( pNtk2 );
     // convert it into an AIG
     pGia = Abc_NtkClpGia( pStrash );
-    //Gia_AigerWrite( pGia, "aig_dump.aig", 0, 0 );
+    //Gia_AigerWrite( pGia, "aig_dump.aig", 0, 0, 0 );
     Abc_NtkDelete( pStrash );
     // get the new network
     Abc_NtkExpandCubes( pNtk, pGia, fVerbose );
@@ -16857,7 +16857,7 @@ int Abc_CommandRecDump3( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_Print( 0, "No structure in the library.\n" );
             return 1;
         }
-        Gia_AigerWrite( pGia, FileName, 0, 0 );
+        Gia_AigerWrite( pGia, FileName, 0, 0, 0 );
     }
     return 0;
 
@@ -30070,9 +30070,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerilog = 0;
     int fMiniAig = 0;
     int fMiniLut = 0;
+    int fWriteNewLine = 0;
     int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "upmlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "upmlcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -30088,6 +30089,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fMiniLut ^= 1;
             break;
+        case 'c':
+            fWriteNewLine ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -30123,16 +30127,17 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     else if ( fMiniLut )
         Gia_ManWriteMiniLut( pAbc->pGia, pFileName );
     else
-        Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
+        Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0, fWriteNewLine );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-upmlvh] <file>\n" );
+    Abc_Print( -2, "usage: &w [-upmlcvh] <file>\n" );
     Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
     Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
     Abc_Print( -2, "\t-p     : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
     Abc_Print( -2, "\t-m     : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
     Abc_Print( -2, "\t-l     : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
+    Abc_Print( -2, "\t-c     : toggle writing \'\\n\' after \'c\' in the AIGER file [default = %s]\n", fWriteNewLine? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
@@ -34710,7 +34715,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
             pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
             Gia_ManStop( pAux );
         }
-        Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 );
+        Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0, 0 );
         Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
         Gia_ManPrintStatsShort( pTemp );
         Gia_ManStop( pTemp );
@@ -34723,7 +34728,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
             pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
             Gia_ManStop( pAux );
 
-            Gia_AigerWrite( pTemp, pFileName2, 0, 0 );
+            Gia_AigerWrite( pTemp, pFileName2, 0, 0, 0 );
             Abc_Print( 1, "Reduced original network was written into file \"%s\".\n", pFileName2 );
             Gia_ManPrintStatsShort( pTemp );
             Gia_ManStop( pTemp );
@@ -34824,7 +34829,7 @@ int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
         Gia_ManStop( pAux );
 
-        Gia_AigerWrite( pTemp, pFileName, 0, 0 );
+        Gia_AigerWrite( pTemp, pFileName, 0, 0, 0 );
         Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
         Gia_ManPrintStatsShort( pTemp );
         Gia_ManStop( pTemp );
@@ -35281,7 +35286,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fDumpMiter )
         {
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
-            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
         }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
         Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
@@ -40538,7 +40543,7 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
         {
             Gia_Man_t * pOne = Gia_ManDupDfsCone( pAbc->pGia, pObj );
             sprintf( Buffer, "%s_%0*d.aig", Extra_FileNameGeneric(pAbc->pGia->pSpec), nDigits, i );
-            Gia_AigerWrite( pOne, Buffer, 0, 0 );
+            Gia_AigerWrite( pOne, Buffer, 0, 0, 0 );
             Gia_ManStop( pOne );
         }
         printf( "Dumped all outputs into individual AIGER files.\n" );
@@ -42929,8 +42934,8 @@ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv )
             sprintf( pName1, "%s_2.aig", pGen );
             ABC_FREE( pGen );
         }
-        Gia_AigerWrite( pPart1, pName0, 0, 0 );
-        Gia_AigerWrite( pPart2, pName1, 0, 0 );
+        Gia_AigerWrite( pPart1, pName0, 0, 0, 0 );
+        Gia_AigerWrite( pPart2, pName1, 0, 0, 0 );
         Gia_ManStop( pPart1 );
         Gia_ManStop( pPart2 );
         if ( fDumpFilesTwo )
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index 7adbed5d..089d3fe2 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -914,7 +914,7 @@ Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t
             int i, nConfLimit = 10000;
             Vec_Int_t * vPat = NULL;
             int status, iVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
-            //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0 );
+            //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0, 0 );
             Gia_ManStop( pGia );
             Cnf_DataFree( pCnf );
             status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index 3f68b815..c850cc56 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -170,7 +170,7 @@ void Abc_NtkTestPinGia( Abc_Ntk_t * pNtk, int fWhiteBoxOnly, int fVerbose )
     Gia_Man_t * pGia;
     char * pFileName = "testpin.aig";
     pGia = Abc_NtkTestPinDeriveGia( pNtk, fWhiteBoxOnly, fVerbose );
-    Gia_AigerWrite( pGia, pFileName, 0, 0 );
+    Gia_AigerWrite( pGia, pFileName, 0, 0, 0 );
     Gia_ManStop( pGia );
     printf( "AIG with pins derived from mapped network \"%s\" was written into file \"%s\".\n", 
         Abc_NtkName(pNtk), pFileName );
@@ -391,7 +391,7 @@ Gia_Man_t * Abc_NtkTestTimDeriveGia( Abc_Ntk_t * pNtk, int fVerbose )
     Vec_FltFree( vArrTimes );
     Vec_FltFree( vReqTimes );
 
-Gia_AigerWrite( pHoles, "holes00.aig", 0, 0 );
+Gia_AigerWrite( pHoles, "holes00.aig", 0, 0, 0 );
 
     // return 
     pGia->pAigExtra = pHoles;
@@ -560,7 +560,7 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
         Gia_ManReverseClasses( pGia, 0 );
     }
     // write file
-    Gia_AigerWrite( pGia, pFileName, 0, 0 );
+    Gia_AigerWrite( pGia, pFileName, 0, 0, 0 );
     // unnormalize choices
     if ( Gia_ManHasChoices(pGia) )
         Gia_ManReverseClasses( pGia, 1 );
diff --git a/src/base/acb/acbCom.c b/src/base/acb/acbCom.c
index c2eae924..3d62454d 100644
--- a/src/base/acb/acbCom.c
+++ b/src/base/acb/acbCom.c
@@ -664,7 +664,7 @@ int Acb_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fDumpMiter )
         {
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
-            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
         }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
         //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index 1efb5807..f6fcf2b0 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -2036,14 +2036,14 @@ Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars )
         Gia_ManStop( p );
         pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
         Gia_ManStop( p );
-        Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0 );
-        Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0 );
+        Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0, 0 );
+        Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0, 0 );
         Gia_ManStop( pCof0 );
         Gia_ManStop( pCof1 );
         printf( "Dumped cof0 into file \"%s\".\n", "eco_qbf0.aig" );
         printf( "Dumped cof1 into file \"%s\".\n", "eco_qbf1.aig" );
     }
-//    Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0 );
+//    Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0, 0 );
 //    printf( "Dumped the result of quantification into file \"%s\".\n", "eco_qbf.aig" );
     pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 0, 0, 0 );
     Gia_ManStop( pCof );
@@ -2445,7 +2445,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
     // generate output files
     Acb_GenerateFilePatch( vPatch, "patch.v" );
     Acb_GenerateFileOut( vInst, pFileNameF, "out.v", vPatch );
-    //Gia_AigerWrite( pGiaG, "test.aig", 0, 0 );
+    //Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 );
 cleanup:
     // cleanup
     if ( vGias )
diff --git a/src/base/bac/bacCom.c b/src/base/bac/bacCom.c
index e7d94d54..f1e3be5f 100644
--- a/src/base/bac/bacCom.c
+++ b/src/base/bac/bacCom.c
@@ -651,7 +651,7 @@ int Bac_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fDumpMiter )
         {
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
-            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
         }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
         //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index b6a8c802..fa13030a 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -662,7 +662,7 @@ int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fDumpMiter )
         {
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
-            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+            Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
         }
         pAbc->Status = Cec_ManVerify( pMiter, pPars );
         //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index ab517ed8..efee671d 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -502,7 +502,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // create input file
-    Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0 );
+    Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0, 0 );
 
     // create command line
     vCommand = Vec_StrAlloc( 100 );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 4b59379b..c5c351c4 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -2361,8 +2361,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
         assert( Gia_ManPoNum(pNew) % 2 == 0 );
         sprintf( pFileName0, "%s_lhs_.aig", pNameGeneric );
         sprintf( pFileName1, "%s_rhs_.aig", pNameGeneric );
-        Gia_AigerWrite( pGia0, pFileName0, 0, 0 );
-        Gia_AigerWrite( pGia1, pFileName1, 0, 0 );
+        Gia_AigerWrite( pGia0, pFileName0, 0, 0, 0 );
+        Gia_AigerWrite( pGia1, pFileName1, 0, 0, 0 );
         Gia_ManStop( pGia0 );
         Gia_ManStop( pGia1 );
         Vec_IntFree( vOrder );
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
index ccc319e5..fd844b62 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -1006,7 +1006,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
         if ( fDumpAbs )
         {
             char * pFileName = "mem_abs.aig";
-            Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+            Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
             printf( "Iteration %3d: Dumped abstraction in file \"%s\" after finding CEX in frame %d.\n", nIters, pFileName, pCex ? pCex->iFrame : -1 );
         }
 
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 42332819..d8187bd4 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1663,7 +1663,7 @@ void Io_ReadWordTest( char * pFileName )
     Wlc_WriteVer( pNtk, "test.v", 0, 0 );
 
     pNew = Wlc_NtkBitBlast( pNtk, NULL );
-    Gia_AigerWrite( pNew, "test.aig", 0, 0 );
+    Gia_AigerWrite( pNew, "test.aig", 0, 0, 0 );
     Gia_ManStop( pNew );
 
     Wlc_NtkFree( pNtk );
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index d1ed7abd..13e45f47 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -622,10 +622,10 @@ sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t **
     sat_solver * pSat = NULL;
     *pvPiVars = *pvPoVars = NULL;
     p1 = Ifn_ManStrFindModel( p );
-//    Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
+//    Gia_AigerWrite( p1, "satbuild.aig", 0, 0, 0 );
     p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
     Gia_ManStop( p1 );
-//    Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
+//    Gia_AigerWrite( p2, "satbuild2.aig", 0, 0, 0 );
     pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
     Gia_ManStop( p2 );
     return pSat;
diff --git a/src/misc/extra/extraUtilPath.c b/src/misc/extra/extraUtilPath.c
index c7231a05..165f4022 100644
--- a/src/misc/extra/extraUtilPath.c
+++ b/src/misc/extra/extraUtilPath.c
@@ -98,7 +98,7 @@ void Abc_EnumeratePathsTest()
 {
     int nSize = 2;
     Gia_Man_t * pGia = Abc_EnumeratePaths( nSize );
-    Gia_AigerWrite( pGia, "testpath.aig", 0, 0 );
+    Gia_AigerWrite( pGia, "testpath.aig", 0, 0, 0 );
     Gia_ManStop( pGia );
 }
 
@@ -353,7 +353,7 @@ void Abc_GraphDeriveGiaDump( Vec_Wec_t * vNodes, Vec_Int_t * vEdges, int Size )
     char pFileName[100];
     Gia_Man_t * pGia = Abc_GraphDeriveGia( vNodes, vEdges );
     sprintf( pFileName, "grid_%dx%d_e%03d.aig", Size, Size, Vec_IntSize(vEdges)/2 );
-    Gia_AigerWrite( pGia, pFileName, 0, 0 );
+    Gia_AigerWrite( pGia, pFileName, 0, 0, 0 );
     Gia_ManStop( pGia );
     printf( "Finished dumping AIG into file \"%s\".\n", pFileName );
 }
diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c
index f988b656..ecf87653 100644
--- a/src/misc/util/utilBridge.c
+++ b/src/misc/util/utilBridge.c
@@ -551,7 +551,7 @@ void Gia_ManFromBridgeTest( char * pFileName )
     fclose ( pFile );
 
     Gia_ManPrintStats( p, NULL );
-    Gia_AigerWrite( p, "temp.aig", 0, 0 );
+    Gia_AigerWrite( p, "temp.aig", 0, 0, 0 );
 
     Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
     Gia_ManStop( p );
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 698d415b..bd6b8c76 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1430,7 +1430,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         // dump abstraction map
         Vec_IntFreeP( &p->pGia->vGateClasses );
         p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
-        Gia_AigerWrite( p->pGia, pFileName, 0, 0 );
+        Gia_AigerWrite( p->pGia, pFileName, 0, 0, 0 );
     }
     else if ( p->pPars->fDumpVabs )
     {
@@ -1443,7 +1443,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
         vGateClasses = Ga2_ManAbsTranslate( p );
         pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
         Gia_ManCleanValue( p->pGia );
-        Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+        Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
         Gia_ManStop( pAbs );
         Vec_IntFreeP( &vGateClasses );
     }
@@ -1563,7 +1563,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
                     Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
                 Gia_ManForEachRo( pAig, pObj, i )
                     Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
-                Gia_AigerWrite( pAig, pFileName, 0, 0 );
+                Gia_AigerWrite( pAig, pFileName, 0, 0, 0 );
                 Vec_IntFree( pAig->vGateClasses );
                 pAig->vGateClasses = vMap;
                 if ( p->pPars->fVerbose )
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index 70bd2e91..45ed1392 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -1619,7 +1619,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
     pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
     Vec_IntFreeP( &vGateClasses );
     // write into file
-    Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+    Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
     Gia_ManStop( pAbs );
 }
 
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index 01680a3f..597e4b72 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -1439,7 +1439,7 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
     pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
     Vec_IntFreeP( &p->pGia->vGateClasses );
     // send it out
-    Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+    Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
     Gia_ManStop( pAbs );
 }
 
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 1a575fbe..033fbc35 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -527,7 +527,7 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
         if ( fDumpMiter )
         {
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
-            Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0 );
+            Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0, 0 );
         }
         status = Cec_ManVerify( pMiter, pCecPars );
         ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c
index 93ef7f10..4eb79fee 100644
--- a/src/proof/acec/acecOrder.c
+++ b/src/proof/acec/acecOrder.c
@@ -173,7 +173,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
     {        
         Gia_Man_t * pNew;
         pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 );
-        Gia_AigerWrite( pNew, "leftover.aig", 0, 0 );
+        Gia_AigerWrite( pNew, "leftover.aig", 0, 0, 0 );
         printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" );
         Gia_ManStop( pNew );
     }
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index be6df65f..ee45aa6c 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -392,7 +392,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     {
         ABC_FREE( pNew->pReprs );
         ABC_FREE( pNew->pNexts );
-        Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
+        Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0, 0 );
         Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
     }
     if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 250cb69e..b9529658 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -407,7 +407,7 @@ p->timeSim += Abc_Clock() - clk;
         }
         pSrm = Cec_ManFraSpecReduction( p ); 
 
-//        Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
+//        Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0, 0 );
 
         if ( pPars->fVeryVerbose )
             Gia_ManPrintStats( pSrm, NULL );
@@ -493,7 +493,7 @@ p->timeSat += Abc_Clock() - clk;
                     Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
                 if ( fOutputResult )
                 {
-                    Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
+                    Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0, 0 );
                     Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
                 }
             }
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 3bff4d38..fdc60299 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1196,7 +1196,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         pNew = Gia_ManCorrReduce( pAig );
         pNew = Gia_ManSeqCleanup( pTemp = pNew );
         Gia_ManStop( pTemp );
-        //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
+        //Gia_AigerWrite( pNew, "reduced.aig", 0, 0, 0 );
     }
     // report the results
     if ( pPars->fVerbose )
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index f39fb2a4..81420e03 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -401,14 +401,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
         }
 
         // write equivalence classes
-        Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
+        Gia_AigerWrite( pAig, "gore.aig", 0, 0, 0 );
         // reduce the model
         pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
         if ( pReduce )
         {
             pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
             Gia_ManStop( pAux );
-            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
+            Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0, 0 );
 //            Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
 //          Gia_ManPrintStatsShort( pReduce );
             Gia_ManStop( pReduce );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index ee9b8e7d..02f14b76 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -742,7 +742,7 @@ clk2 = Abc_Clock();
         if ( status == -1 )
         {
             Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
-            Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
+            Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0, 0 );
             Gia_ManStop( pTemp );
             Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
         }
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 6e5fd221..94658583 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -309,7 +309,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
         {
             pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
             sprintf( Buffer, "part%03d.aig", i );
-            Gia_AigerWrite( pTemp, Buffer, 0, 0 );
+            Gia_AigerWrite( pTemp, Buffer, 0, 0, 0 );
             Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
                 i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
             Gia_ManStop( pTemp );
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 04d44353..b9c2db2c 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -711,7 +711,7 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     if ( pPars->fDumpFrames )
     {
         p->pFrames = Gia_ManCleanup( p->pFrames );
-        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
         printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
         Gia_ManStop( p->pFrames );
     }
@@ -793,7 +793,7 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         Gia_ManPrintStats( p->pFrames, NULL );
     if ( pPars->fDumpFrames )
     {
-        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
         printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
     }
     for ( f = 0; f < nFramesMax; f++ )
@@ -977,7 +977,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         Gia_ManPrintStats( p->pFrames, NULL );
     if ( pPars->fDumpFrames )
     {
-        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+        Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
         printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
     }
     if ( pPars->fUseOldCnf )
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index 38b57d5f..f0883f9a 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -110,7 +110,7 @@ Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames )
     Gia_ManPrintStats( pNew, NULL );
     pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
     Gia_ManStop( pNew );
-    Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 );
+    Gia_AigerWrite( pTemp, "miter3.aig", 0, 0, 0 );
     return pTemp;
 }
 
@@ -308,7 +308,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
         Vec_PtrPush( vCones, pNew );
     }
     pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
-    Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
+    Gia_AigerWrite( pNew, "miter2.aig", 0, 0, 0 );
 //Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
     Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
         Gia_ManStop( pTemp );
diff --git a/src/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c
index b8514601..b39b8eec 100644
--- a/src/sat/bmc/bmcCexMin2.c
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -334,7 +334,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
         printf( "%3d : ", iFrameStart );
         Gia_ManPrintStats( pNew, NULL );
         if ( fVerbose )
-            Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
+            Gia_AigerWrite( pNew, "temp.aig", 0, 0, 0 );
         Gia_ManStop( pNew );
     }
     else // CEX min
@@ -345,7 +345,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
             printf( "%3d : ", f );
             Gia_ManPrintStats( pNew, NULL );
             if ( fVerbose )
-                Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
+                Gia_AigerWrite( pNew, "temp.aig", 0, 0, 0 );
             Gia_ManStop( pNew );
         }
     }
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 9c80b278..5a29c8bc 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -173,7 +173,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
     abctime clk = Abc_Clock();
     pNew = Bmc_CexPerformUnrolling( p, pCex );
     Gia_ManPrintStats( pNew, NULL );
-    Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
+    Gia_AigerWrite( pNew, "unroll.aig", 0, 0, 0 );
 //Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
     Gia_ManStop( pNew );
     printf( "CE-induced network is written into file \"unroll.aig\".\n" );
@@ -285,7 +285,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
     abctime clk = Abc_Clock();
     pNew = Bmc_CexBuildNetwork( p, pCex );
     Gia_ManPrintStats( pNew, NULL );
-    Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
+    Gia_AigerWrite( pNew, "unate.aig", 0, 0, 0 );
 //Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
     Gia_ManStop( pNew );
     printf( "CE-induced network is written into file \"unate.aig\".\n" );
diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c
index 9d30fc09..b42d527a 100644
--- a/src/sat/bmc/bmcEco.c
+++ b/src/sat/bmc/bmcEco.c
@@ -291,7 +291,7 @@ void Bmc_EcoMiterTest()
         Vec_IntPush( vFans, Gia_ObjId(pOld, pObj) );
     pMiter = Bmc_EcoMiter( pGold, pOld, vFans );
     Vec_IntFree( vFans );
-    Gia_AigerWrite( pMiter, "eco_miter.aig", 0, 0 );
+    Gia_AigerWrite( pMiter, "eco_miter.aig", 0, 0, 0 );
     // find the patch
     RetValue = Bmc_EcoPatch( pMiter, Gia_ManCiNum(pGold), Gia_ManCoNum(pGold) );
     if ( RetValue == 1 )
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 096d8aaa..28d8a0c1 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -754,7 +754,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly )
     Gia_ManStop( pTemp );
     assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * (fFfOnly ? Count : Gia_ManAndNum(p)) );
 //    if ( fUseFaults )
-//        Gia_AigerWrite( pNew, "newfault.aig", 0, 0 );
+//        Gia_AigerWrite( pNew, "newfault.aig", 0, 0, 0 );
     return pNew;
 }
 
@@ -1260,7 +1260,7 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int
         p1 = Gia_ManFOFUnfold( p, vMap );
     if ( pPars->Algo != 1 )
         p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
-//    Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
+//    Gia_AigerWrite( p1, "newfault.aig", 0, 0, 0 );
 //    printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
 
     // create miter
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index 0ad9271b..10513936 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -489,8 +489,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
 
 Gia_ManPrintStats( pFrames0, NULL );
 Gia_ManPrintStats( pFrames1, NULL );
-Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 );
-Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 );
+Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0, 0 );
+Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0, 0 );
 
     Gia_ManStop( pFrames0 );
     Gia_ManStop( pFrames1 );