diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 58131f185..0b70f2dbb 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -214,6 +214,7 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
     Vec_Int_t *       vNameIds;      // name IDs
     Vec_Int_t *       vFins;         // obj/type info
+    Vec_Int_t *       vOrigNodeIds;  // original node IDs
 };
 
 struct Abc_Des_t_ 
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 2c8e03b34..3c8fd383e 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -461,6 +461,15 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
             if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) )
                 Abc_ObjForEachFanin( pObj, pFanin, k )
                     Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+        // move object IDs
+        if ( pNtk->vOrigNodeIds ) 
+        {
+            pNtkNew->vOrigNodeIds = Vec_IntStartFull( Abc_NtkObjNumMax(pNtkNew) );
+            Abc_NtkForEachObj( pNtk, pObj, i )
+                if ( pObj->pCopy && Vec_IntEntry(pNtk->vOrigNodeIds, pObj->Id) > 0 )
+                    Vec_IntWriteEntry( pNtkNew->vOrigNodeIds, pObj->pCopy->Id, Vec_IntEntry(pNtk->vOrigNodeIds, pObj->Id) );
+        }
+        
     }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
@@ -1483,6 +1492,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_IntFreeP( &pNtk->vObjPerm );
     Vec_IntFreeP( &pNtk->vTopo );
     Vec_IntFreeP( &pNtk->vFins );
+    Vec_IntFreeP( &pNtk->vOrigNodeIds );
     ABC_FREE( pNtk );
 }
 
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index efe10a49c..88b8cbf69 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -241,7 +241,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     // add the root node to the cone (for visualization)
     Vec_PtrPush( vCutSmall, pNode );
     // write the DOT file
-    Io_WriteDotNtk( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0, 0 );
+    Io_WriteDotNtk( pNode->pNtk, vInside, vCutSmall, FileNameDot, 0, 0, 0 );
     // stop the cut computation manager
     Abc_NtkManCutStop( p );
 
@@ -260,7 +260,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse, int fKeepDot )
+void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse, int fKeepDot, int fAigIds )
 {
     FILE * pFile;
     Abc_Ntk_t * pNtk;
@@ -302,7 +302,7 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk0, int fGateNames, int fSeq, int fUseReverse,
     if ( fSeq )
         Io_WriteDotSeq( pNtk, vNodes, NULL, FileNameDot, fGateNames, fUseReverse );
     else
-        Io_WriteDotNtk( pNtk, vNodes, NULL, FileNameDot, fGateNames, fUseReverse );
+        Io_WriteDotNtk( pNtk, vNodes, NULL, FileNameDot, fGateNames, fUseReverse, fAigIds );
     pNtk->nBarBufs = nBarBufs;
     Vec_PtrFree( vNodes );
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4251f69d7..36d9b46d3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3220,7 +3220,8 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fUseReverse;
     int fFlopDep;
     int fKeepDot;
-    extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames, int fSeq, int fUseReverse, int fKeepDot );
+    int fAigIds;
+    extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames, int fSeq, int fUseReverse, int fKeepDot, int fAigIds );
     extern void Abc_NtkShowFlopDependency( Abc_Ntk_t * pNtk );
 
     // set defaults
@@ -3229,8 +3230,9 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
     fUseReverse = 1;
     fFlopDep    = 0;
     fKeepDot    = 0;
+    fAigIds     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "rsgfdh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rsgfdih" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3249,6 +3251,9 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fKeepDot ^= 1;
             break;
+        case 'i':
+            fAigIds ^= 1;
+            break;
         default:
             goto usage;
         }
@@ -3263,11 +3268,11 @@ int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fFlopDep )
         Abc_NtkShowFlopDependency( pNtk );
     else
-        Abc_NtkShow( pNtk, fGateNames, fSeq, fUseReverse, fKeepDot );
+        Abc_NtkShow( pNtk, fGateNames, fSeq, fUseReverse, fKeepDot, fAigIds );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: show [-srgfdh]\n" );
+    Abc_Print( -2, "usage: show [-srgfdih]\n" );
     Abc_Print( -2, "       visualizes the network structure using DOT and GSVIEW\n" );
 #ifdef WIN32
     Abc_Print( -2, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
@@ -3278,6 +3283,7 @@ usage:
     Abc_Print( -2, "\t-g    : toggles printing gate names for mapped network [default = %s].\n", fGateNames? "yes": "no" );
     Abc_Print( -2, "\t-f    : toggles visualizing flop dependency graph [default = %s].\n", fFlopDep? "yes": "no" );
     Abc_Print( -2, "\t-d    : toggles keeping the .dot file used to produce the .ps file [default = %s].\n", fKeepDot? "yes": "no" );
+    Abc_Print( -2, "\t-i    : toggles using original AIG object IDs as node labels [default = %s].\n", fAigIds? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index a4205c0ab..326e837c9 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -276,6 +276,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, f
     Map_ManSetAreaRecovery( pMan, fRecovery );
     Map_ManSetOutputNames( pMan, Abc_NtkCollectCioNames(pNtk, 1) );
     Map_ManSetDelayTarget( pMan, (float)DelayTarget );
+    Map_ManCreateAigIds( pMan, Abc_NtkObjNumMax(pNtk) );
 
     // set arrival and requireds
     if ( Scl_ConIsRunning() && Scl_ConHasInArrs() )
@@ -298,6 +299,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, f
         pNode->pCopy = (Abc_Obj_t *)pNodeMap;
         if ( pSwitching )
             Map_NodeSetSwitching( pNodeMap, pSwitching[pNode->Id] );
+        Map_NodeSetAigId( pNodeMap, pNode->Id );
     }
 
     // load the AIG into the mapper
@@ -328,6 +330,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, f
                 Map_NodeSetNextE( (Map_Node_t *)pPrev->pCopy, (Map_Node_t *)pFanin->pCopy );
                 Map_NodeSetRepr( (Map_Node_t *)pFanin->pCopy, (Map_Node_t *)pNode->pCopy );
             }
+        Map_NodeSetAigId( pNodeMap, pNode->Id );
     }
     assert( Map_ManReadBufNum(pMan) == pNtk->nBarBufs );
     Vec_PtrFree( vNodes );
@@ -432,6 +435,7 @@ Abc_Obj_t * Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap
 
     // implement the supergate
     pNodeNew = Abc_NodeFromMapSuper_rec( pNtkNew, pNodeMap, pSuperBest, pNodePIs, nLeaves );
+    Vec_IntWriteEntry( pNtkNew->vOrigNodeIds, pNodeNew->Id, Abc_Var2Lit( Map_NodeReadAigId(pNodeMap), fPhase ) );
     Map_NodeSetData( pNodeMap, fPhase, (char *)pNodeNew );
     return pNodeNew;
 }
@@ -463,6 +467,7 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int
 
     // add the inverter
     pNodeInv = Abc_NtkCreateNode( pNtkNew );
+    Vec_IntWriteEntry( pNtkNew->vOrigNodeIds, pNodeInv->Id, Abc_Var2Lit( Map_NodeReadAigId(pNodeMap), fPhase ) );
     Abc_ObjAddFanin( pNodeInv, pNodeNew );
     pNodeInv->pData = Mio_LibraryReadInv((Mio_Library_t *)Abc_FrameReadLibGen());
 
@@ -479,6 +484,7 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk, int fUseBuffs )
     assert( Map_ManReadBufNum(pMan) == pNtk->nBarBufs );
     // create the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
+    pNtkNew->vOrigNodeIds = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
     // make the mapper point to the new network
     Map_ManCleanData( pMan );
     Abc_NtkForEachCi( pNtk, pNode, i )
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index 9758f1963..9a0d82098 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -121,7 +121,7 @@ extern void               Io_WriteBook( Abc_Ntk_t * pNtk, char * FileName );
 extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes );
 /*=== abcWriteDot.c ===========================================================*/
 extern void               Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName );
-extern void               Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse );
+extern void               Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse, int fAigIds );
 extern void               Io_WriteDotSeq( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse );
 /*=== abcWriteEqn.c ===========================================================*/
 extern void               Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 0ab3c4d2f..a5ba4c178 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -52,7 +52,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName )
 {
     Vec_Ptr_t * vNodes;
     vNodes = Abc_NtkCollectObjects( pNtk );
-    Io_WriteDotNtk( pNtk, vNodes, NULL, FileName, 0, 0 );
+    Io_WriteDotNtk( pNtk, vNodes, NULL, FileName, 0, 0, 0 );
     Vec_PtrFree( vNodes );
 }
 
@@ -68,12 +68,12 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse )
+void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse, int fAigIds )
 {
     FILE * pFile;
     Abc_Obj_t * pNode, * pFanin;
     char * pSopString;
-    int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
+    int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev, AigNodeId;
     int Limit = 500;
 
     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
@@ -304,7 +304,13 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
                 pSopString = Abc_NtkPrintSop(Mio_GateReadSop((Mio_Gate_t *)pNode->pData));
             else
                 pSopString = Abc_NtkPrintSop((char *)pNode->pData);
-            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
+            //if ( pNtk->vOrigNodeIds )
+            //    printf( "%d = %d \n", pNode->Id, Vec_IntEntry(pNtk->vOrigNodeIds, pNode->Id) )
+            AigNodeId = (fAigIds && pNtk->vOrigNodeIds) ? Vec_IntEntry(pNtk->vOrigNodeIds, pNode->Id) : -1;
+            if ( AigNodeId > 0 )
+                fprintf( pFile, "  Node%d [label = \"%s%d\\n%s\"", pNode->Id, Abc_LitIsCompl(AigNodeId) ? "-":"+", Abc_Lit2Var(AigNodeId), pSopString );
+            else 
+                fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
 //            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, 
 //                SuppSize, 
 //                pSopString );
diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h
index 03ac30635..97115f666 100644
--- a/src/map/mapper/mapper.h
+++ b/src/map/mapper/mapper.h
@@ -110,11 +110,13 @@ extern void            Map_ManSetVerbose( Map_Man_t * p, int fVerbose );
 extern void            Map_ManSetSwitching( Map_Man_t * p, int fSwitching );
 extern void            Map_ManSetSkipFanout( Map_Man_t * p, int fSkipFanout );
 extern void            Map_ManSetUseProfile( Map_Man_t * p );
+extern void            Map_ManCreateAigIds( Map_Man_t * p, int nObjs );   
 
 extern Map_Man_t *     Map_NodeReadMan( Map_Node_t * p );
 extern char *          Map_NodeReadData( Map_Node_t * p, int fPhase );
 extern int             Map_NodeReadNum( Map_Node_t * p );
 extern int             Map_NodeReadLevel( Map_Node_t * p );
+extern int             Map_NodeReadAigId( Map_Node_t * p );
 extern Map_Cut_t *     Map_NodeReadCuts( Map_Node_t * p );
 extern Map_Cut_t *     Map_NodeReadCutBest( Map_Node_t * p, int fPhase );
 extern Map_Node_t *    Map_NodeReadOne( Map_Node_t * p );
@@ -123,6 +125,7 @@ extern void            Map_NodeSetData( Map_Node_t * p, int fPhase, char * pData
 extern void            Map_NodeSetNextE( Map_Node_t * p, Map_Node_t * pNextE );
 extern void            Map_NodeSetRepr( Map_Node_t * p, Map_Node_t * pRepr );
 extern void            Map_NodeSetSwitching( Map_Node_t * p, float Switching );
+extern void            Map_NodeSetAigId( Map_Node_t * p, int Id );
 
 extern int             Map_NodeIsConst( Map_Node_t * p );
 extern int             Map_NodeIsVar( Map_Node_t * p );
diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c
index d3e574f34..4a651991d 100644
--- a/src/map/mapper/mapperCreate.c
+++ b/src/map/mapper/mapperCreate.c
@@ -75,6 +75,7 @@ void            Map_ManSetVerbose( Map_Man_t * p, int fVerbose )           { p->
 void            Map_ManSetSwitching( Map_Man_t * p, int fSwitching )       { p->fSwitching = fSwitching; }   
 void            Map_ManSetSkipFanout( Map_Man_t * p, int fSkipFanout )     { p->fSkipFanout = fSkipFanout; }   
 void            Map_ManSetUseProfile( Map_Man_t * p )                      { p->fUseProfile = 1;         }   
+void            Map_ManCreateAigIds( Map_Man_t * p, int nObjs )            { p->pAigNodeIDs = ABC_CALLOC( int, nObjs ); }   
 
 /**Function*************************************************************
 
@@ -91,6 +92,7 @@ Map_Man_t *     Map_NodeReadMan( Map_Node_t * p )                     { return p
 char *          Map_NodeReadData( Map_Node_t * p, int fPhase )        { return fPhase? p->pData1 : p->pData0;  }
 int             Map_NodeReadNum( Map_Node_t * p )                     { return p->Num;                }
 int             Map_NodeReadLevel( Map_Node_t * p )                   { return Map_Regular(p)->Level; }
+int             Map_NodeReadAigId( Map_Node_t * p )                   { return p->p->pAigNodeIDs[p->Num]; }
 Map_Cut_t *     Map_NodeReadCuts( Map_Node_t * p )                    { return p->pCuts;              }
 Map_Cut_t *     Map_NodeReadCutBest( Map_Node_t * p, int fPhase )     { return p->pCutBest[fPhase];   }
 Map_Node_t *    Map_NodeReadOne( Map_Node_t * p )                     { return p->p1;                 }
@@ -99,6 +101,10 @@ void            Map_NodeSetData( Map_Node_t * p, int fPhase, char * pData ) { if
 void            Map_NodeSetNextE( Map_Node_t * p, Map_Node_t * pNextE )     { p->pNextE = pNextE;       }
 void            Map_NodeSetRepr( Map_Node_t * p, Map_Node_t * pRepr )       { p->pRepr = pRepr;         }
 void            Map_NodeSetSwitching( Map_Node_t * p, float Switching )     { p->Switching = Switching; }
+void            Map_NodeSetAigId( Map_Node_t * p, int Id )            { p->p->pAigNodeIDs[p->Num] = Id; }
+
+;
+
 
 /**Function*************************************************************
 
@@ -261,6 +267,7 @@ void Map_ManFree( Map_Man_t * p )
     if ( p->pCounters ) ABC_FREE( p->pCounters );
     Extra_MmFixedStop( p->mmNodes );
     Extra_MmFixedStop( p->mmCuts );
+    ABC_FREE( p->pAigNodeIDs );
     ABC_FREE( p->pNodeDelays );
     ABC_FREE( p->pInputArrivals );
     ABC_FREE( p->pOutputRequireds );
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index 79c8d61ad..768255a8a 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -107,6 +107,7 @@ struct Map_ManStruct_t_
     char **             ppOutputNames; // the primary output names
     Map_Time_t *        pInputArrivals;// the PI arrival times
     Map_Time_t *        pOutputRequireds;// the PI arrival times
+    int *               pAigNodeIDs;   // IDs of the original AIG nodes
 
     // mapping parameters
     int                 nVarsMax;      // the max number of variables