Enabled recording the name of the file GIA is coming from.

src/aig/gia/gia.h

@@ -100,6 +100,7 @@ typedef struct Gia_Man_t_ Gia_Man_t;
 struct Gia_Man_t_
 {
     char *         pName;         // name of the AIG
+    char *         pSpec;         // name of the input file
     int            nRegs;         // number of registers
     int            nRegsAlloc;    // number of allocated registers
     int            nObjs;         // number of objects

src/aig/gia/giaAbsGla.c

@@ -966,6 +966,7 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping )
     // start new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // start mapping
     Gia_ManFillValue( p );
     pObj2Obj = ABC_FALLOC( int, Gia_ManObjNum(p) );

src/aig/gia/giaAig.c

@@ -90,6 +90,7 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
     if ( p->pEquivs )
@@ -129,6 +130,7 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
@@ -168,6 +170,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );

src/aig/gia/giaAiger.c

@@ -447,6 +447,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
     pName = Gia_FileNameGeneric( pFileName );
     pNew->pName = Abc_UtilStrsav( pName );
+    pNew->pSpec = Abc_UtilStrsav( pFileName );
 //    pNew->pSpec = Abc_UtilStrsav( pFileName );
     ABC_FREE( pName );
     pNew->nConstrs = nConstr;
@@ -1097,6 +1098,8 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck )
 //        pNew->pSpec = Ioa_UtilStrsav( pFileName );
         ABC_FREE( pName );
     }
+    assert( pNew->pSpec == NULL );
+    pNew->pSpec = Abc_UtilStrsav( pFileName );
     return pNew;
 }
 

src/aig/gia/giaBidec.c

@@ -260,6 +260,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
 //    Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
     pManDec = Bdc_ManAlloc( pPars );

src/aig/gia/giaCof.c

@@ -718,6 +718,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
     }
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;

src/aig/gia/giaDup.c

@@ -174,6 +174,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -206,6 +207,7 @@ Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     for ( i = iOutStart; i < iOutStop; i++ )
     {
@@ -265,6 +267,7 @@ Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -298,6 +301,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCoReverse( p, pObj, i )
         Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -330,6 +334,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -362,6 +367,7 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -404,6 +410,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -438,6 +445,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
     int i, iCtrl;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -478,6 +486,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
     assert( p->vFlopClasses != NULL );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachPi( p, pObj, i )
@@ -523,6 +532,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->nConstrs = p->nConstrs;
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -589,6 +599,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
     assert( nTimes > 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
     vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
@@ -699,6 +710,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManDupDfs2_rec( pNew, p, pObj );
@@ -757,6 +769,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -790,6 +803,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -820,6 +834,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -848,6 +863,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -878,6 +894,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -946,6 +963,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD
     // start new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // check if there are PIs to be added
     Gia_ManCreateRefs( p );
     Gia_ManForEachPi( p, pObj, i )
@@ -1022,6 +1040,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p )
     // start new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // check if there are PIs to be added
     Gia_ManCreateRefs( p );
     // discount references of POs
@@ -1076,6 +1095,7 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
     assert( Gia_ManRegNum(p2) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p)+Gia_ManObjNum(p2) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     // dup first AIG
     Gia_ManConst0(p)->Value = 0;
@@ -1138,6 +1158,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
     {
@@ -1188,6 +1209,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -1505,6 +1527,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
     assert( (Gia_ManPoNum(p) & 1) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCi( p, pObj, i )
@@ -1577,6 +1600,7 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
     // start the new manager
     pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
     pNew->pName = Abc_UtilStrsav( pGia0->pName );
+    pNew->pSpec = Abc_UtilStrsav( pGia0->pSpec );
     // create new CIs and assign them to the old manager CIs
     for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
     {
@@ -1618,6 +1642,7 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
     int i, nConstr = 0;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -1679,6 +1704,7 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
     // start the new manager
     pNew = Gia_ManStart( 5000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create PIs
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachPi( p, pObj, i )
@@ -1839,6 +1865,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
     // start the new manager
     pNew = Gia_ManStart( 5000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create constant
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -1947,6 +1974,7 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis )
 //    Gia_ManFillValue( p );
     pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1);
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // map the constant node
     Gia_ManConst0(p)->Value = 0;
     // create PIs

src/aig/gia/giaEnable.c

@@ -366,6 +366,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
     p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
         Gia_ObjSetCopyF( p, 0, pObj, 0 );
@@ -441,6 +442,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -611,6 +613,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
 
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {

src/aig/gia/giaEquiv.c

@@ -475,6 +475,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
         Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -848,6 +849,7 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -918,6 +920,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
         Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -1064,6 +1067,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
         Gia_ManEquivSetColors( p, 0 );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
         Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) );
@@ -1573,6 +1577,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
     assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );

src/aig/gia/giaFrames.c

@@ -112,6 +112,7 @@ Gia_Man_t * Gia_ManUnrollDup( Gia_Man_t * p, Vec_Int_t * vLimit )
     assert( Vec_IntSize(vLimit) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
 
     // save constant class
     Gia_ManFillValue( p );
@@ -408,6 +409,7 @@ void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     assert( p->pNew == NULL );
     p->pNew = Gia_ManStart( 10000 );
     p->pNew->pName = Abc_UtilStrsav( p->pAig->pName );
+    p->pNew->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
     Gia_ManHashAlloc( p->pNew );
     // create combinational inputs
     if ( !p->pPars->fSaveLastLit ) // only in the case when unrolling depth is known
@@ -544,6 +546,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
     // start timeframes
     pNew = Gia_ManStart( 10000 );
     pNew->pName = Abc_UtilStrsav( p->pAig->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
     Gia_ManHashAlloc( pNew );
     // create combinational inputs
     for ( f = 0; f < p->pPars->nFrames; f++ )
@@ -757,6 +760,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+
         Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) );
     pFrames->pName = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
     Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
     for ( f = 0; f < pPars->nFrames; f++ )
@@ -867,6 +871,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
         return Gia_ManFramesInit( pAig, pPars );
     pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
     pFrames->pName = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
     Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
     for ( f = 0; f < pPars->nFrames; f++ )
@@ -937,6 +942,7 @@ Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbos
         printf( "Computing specialized unrolling with %d frames...\n", nFrames );
     pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
     pFrames->pName = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
     Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
     for ( f = 0; nFrames == 0 || f < nFrames; f++ )

src/aig/gia/giaFront.c

@@ -116,6 +116,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit); 
     // start the frontier
     pFront = ABC_CALLOC( char, pNew->nFront );

src/aig/gia/giaGiarf.c

@@ -539,6 +539,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR
     // copy unmarked nodes
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);

src/aig/gia/giaHash.c

@@ -602,6 +602,7 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->fAddStrash = fAddStrash;
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;

src/aig/gia/giaHcd.c

@@ -333,6 +333,7 @@ Gia_Man_t * Hcd_ManChoiceMiter( Vec_Ptr_t * vGias )
     // start the new manager
     pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
     pNew->pName = Abc_UtilStrsav( pGia0->pName );
+    pNew->pSpec = Abc_UtilStrsav( pGia0->pSpec );
     // create new CIs and assign them to the old manager CIs
     for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
     {
@@ -564,6 +565,7 @@ Gia_Man_t * Hcd_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )

src/aig/gia/giaIso.c

@@ -953,6 +953,7 @@ Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAn
     // start the new manager
     pNew = Gia_ManStart( 5000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create constant
     Gia_ManConst0(p)->Value = 0;
     // create PIs

src/aig/gia/giaMan.c

@@ -105,11 +105,12 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pReprsOld );
     ABC_FREE( p->pReprs );
     ABC_FREE( p->pNexts );
-    ABC_FREE( p->pName );
     ABC_FREE( p->pRefs );
     ABC_FREE( p->pNodeRefs );
     ABC_FREE( p->pHTable );
     ABC_FREE( p->pObjs );
+    ABC_FREE( p->pSpec );
+    ABC_FREE( p->pName );
     ABC_FREE( p );
 }
 

src/aig/gia/giaReparam.c

@@ -53,6 +53,7 @@ Gia_Man_t * Gia_ManDupIn2Ff( Gia_Man_t * p )
     vPiOuts = Vec_IntAlloc( Gia_ManPiNum(p) );
     pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManPiNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachPi( p, pObj, i )
@@ -113,6 +114,7 @@ Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld )
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachRo( p, pObj, i )

src/aig/gia/giaRetime.c

@@ -126,6 +126,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
     // create the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     // create the true PIs
     Gia_ManFillValue( p );

src/aig/gia/giaShrink.c

@@ -77,6 +77,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
     Gia_ManForEachObj1( p, pObj, i )

src/base/abc/abcHieCec.c

@@ -268,6 +268,7 @@ Gia_Man_t * Abc_NtkDeriveFlatGia( Abc_Ntk_t * pNtk )
     // start the network
     pGia = Gia_ManStart( (1<<16) );
     pGia->pName = Abc_UtilStrsav( Abc_NtkName(pNtk) );
+    pGia->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk) );
     Gia_ManHashAlloc( pGia );
     // create PIs
     Abc_NtkForEachPi( pNtk, pTerm, i )
@@ -344,6 +345,7 @@ Gia_Man_t * Abc_NtkDeriveFlatGia2Derive( Abc_Ntk_t * pNtk, Vec_Ptr_t * vOrder )
     // start the network
     pGia = Gia_ManStart( (1<<15) );
     pGia->pName = Abc_UtilStrsav( Abc_NtkName(pNtk) );
+    pGia->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk) );
     Gia_ManHashAlloc( pGia );
     // create PIs
     Abc_NtkForEachPi( pNtk, pTerm, i )

src/base/abc/abcHieNew.c

@@ -1226,6 +1226,7 @@ Gia_Man_t * Au_NtkDeriveFlatGia( Au_Ntk_t * p )
     // start the network
     pGia = Gia_ManStart( (1<<16) );
     pGia->pName = Abc_UtilStrsav( Au_NtkName(p) );
+//    pGia->pSpec = Abc_UtilStrsav( Au_NtkSpec(p) );
     Gia_ManHashAlloc( pGia );
     Gia_ManFlipVerbose( pGia );
     // create PIs

src/opt/mfs/mfsGia.c

@@ -59,6 +59,7 @@ Gia_Man_t * Gia_ManCreateResubMiter( Aig_Man_t * p )
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pSpec = Gia_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     // create the objects
     pOuts0 = ABC_ALLOC( int, Aig_ManPoNum(p) );

src/proof/cec/cecChoice.c

@@ -104,6 +104,7 @@ Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fR
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )

src/proof/cec/cecCorr.c

@@ -116,6 +116,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
     Gia_ManForEachRo( p, pObj, i )
@@ -232,6 +233,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
     {
@@ -693,6 +695,7 @@ Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )

src/proof/cec/cecSweep.c

@@ -54,6 +54,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
         Gia_ManLevelNum( p->pAig );
     pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
     pNew->pName = Abc_UtilStrsav( p->pAig->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pAig->pName );
     Gia_ManHashAlloc( pNew );
     piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
     pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );