Version abc80329

21 files changed, 680 insertions, 1032 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8a61a530..f58ba409 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -47,7 +47,6 @@ extern "C" {
 
 typedef struct Aig_Man_t_            Aig_Man_t;
 typedef struct Aig_Obj_t_            Aig_Obj_t;
-typedef struct Aig_Box_t_            Aig_Box_t;
 typedef struct Aig_MmFixed_t_        Aig_MmFixed_t;    
 typedef struct Aig_MmFlex_t_         Aig_MmFlex_t;     
 typedef struct Aig_MmStep_t_         Aig_MmStep_t;     
@@ -61,9 +60,7 @@ typedef enum {
     AIG_OBJ_BUF,                     // 4: buffer node
     AIG_OBJ_AND,                     // 5: AND node
     AIG_OBJ_EXOR,                    // 6: EXOR node
-    AIG_OBJ_LATCH,                   // 7: latch
-    AIG_OBJ_BOX,                     // 8: latch
-    AIG_OBJ_VOID                     // 9: unused object
+    AIG_OBJ_VOID                     // 7: unused object
 } Aig_Type_t;
 
 // the AIG node
@@ -73,11 +70,11 @@ struct Aig_Obj_t_  // 8 words
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
     Aig_Obj_t *      pHaig;          // pointer to the HAIG node
-    unsigned int     Type    :  4;   // object type
+    unsigned int     Type    :  3;   // object type
     unsigned int     fPhase  :  1;   // value under 000...0 pattern
     unsigned int     fMarkA  :  1;   // multipurpose mask
     unsigned int     fMarkB  :  1;   // multipurpose mask
-    unsigned int     nRefs   : 25;   // reference count 
+    unsigned int     nRefs   : 26;   // reference count 
     unsigned         Level   : 24;   // the level of this node
     unsigned         nCuts   :  8;   // the number of cuts
     int              TravId;         // unique ID of last traversal involving the node
@@ -89,16 +86,6 @@ struct Aig_Obj_t_  // 8 words
     };
 };
 
-// the AIG box
-struct Aig_Box_t_  
-{
-    int              nInputs;        // the number of box inputs (POs)
-    int              i1Input;        // the first PO of the interval
-    int              nOutputs;       // the number of box outputs (PIs)
-    int              i1Output;       // the first PI of the interval
-    float **         pTable;         // the delay table of the box
-};
-
 // the AIG manager
 struct Aig_Man_t_
 {
@@ -154,7 +141,6 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
     void *           pSeqModel;
-    Aig_Man_t *      pManHaig;
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
     // timing statistics
@@ -265,7 +251,6 @@ static inline int          Aig_ManPoNum( Aig_Man_t * p )          { return p->nO
 static inline int          Aig_ManBufNum( Aig_Man_t * p )         { return p->nObjs[AIG_OBJ_BUF];                    }
 static inline int          Aig_ManAndNum( Aig_Man_t * p )         { return p->nObjs[AIG_OBJ_AND];                    }
 static inline int          Aig_ManExorNum( Aig_Man_t * p )        { return p->nObjs[AIG_OBJ_EXOR];                   }
-static inline int          Aig_ManLatchNum( Aig_Man_t * p )       { return p->nObjs[AIG_OBJ_LATCH];                  }
 static inline int          Aig_ManNodeNum( Aig_Man_t * p )        { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR];   }
 static inline int          Aig_ManGetCost( Aig_Man_t * p )        { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
 static inline int          Aig_ManObjNum( Aig_Man_t * p )         { return p->nCreated - p->nDeleted;                }
@@ -289,10 +274,9 @@ static inline int          Aig_ObjIsPo( Aig_Obj_t * pObj )        { return pObj-
 static inline int          Aig_ObjIsBuf( Aig_Obj_t * pObj )       { return pObj->Type == AIG_OBJ_BUF;    }
 static inline int          Aig_ObjIsAnd( Aig_Obj_t * pObj )       { return pObj->Type == AIG_OBJ_AND;    }
 static inline int          Aig_ObjIsExor( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_EXOR;   }
-static inline int          Aig_ObjIsLatch( Aig_Obj_t * pObj )     { return pObj->Type == AIG_OBJ_LATCH;  }
 static inline int          Aig_ObjIsNode( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR;   }
 static inline int          Aig_ObjIsTerm( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_PI  || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1;   }
-static inline int          Aig_ObjIsHash( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH;  }
+static inline int          Aig_ObjIsHash( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR;                                 }
 static inline int          Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0;                    }
 
 static inline int          Aig_ObjIsMarkA( Aig_Obj_t * pObj )     { return pObj->fMarkA;  }
@@ -405,6 +389,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 // iterator over all nodes
 #define Aig_ManForEachNode( p, pObj, i )                                        \
     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
+// iterator over all nodes
+#define Aig_ManForEachExor( p, pObj, i )                                        \
+    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
 // iterator over the nodes whose IDs are stored in the array
 #define Aig_ManForEachNodeVec( p, vIds, pObj, i )                               \
     for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
@@ -458,6 +445,7 @@ extern Aig_ManCut_t *  Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLea
 extern void            Aig_ManCutStop( Aig_ManCut_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
+extern Vec_Vec_t *     Aig_ManLevelize( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
@@ -514,7 +502,6 @@ extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_O
 extern Aig_Obj_t *     Aig_IthVar( Aig_Man_t * p, int i );
 extern Aig_Obj_t *     Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
 extern Aig_Obj_t *     Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
-extern Aig_Obj_t *     Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne );
 extern Aig_Obj_t *     Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
 extern Aig_Obj_t *     Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
 extern Aig_Obj_t *     Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
@@ -564,9 +551,7 @@ extern Aig_Man_t *     Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
 extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
 extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
-extern void            Aig_ManComputeSccs( Aig_Man_t * p );
-/*=== aigSeq.c ========================================================*/
-extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
+extern void            Aig_ManComputeSccs( Aig_Man_t * p ); 
 /*=== aigShow.c ========================================================*/
 extern void            Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
 /*=== aigTable.c ========================================================*/
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index 8c53e635..bddc9288 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -90,23 +90,23 @@ int Aig_ManCheck( Aig_Man_t * p )
     }
     // count the total number of nodes
     if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + 
-        Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
+        Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) )
     {
         printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
-        printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
-            1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p), 
-            1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) );
+        printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Total = %d.\n",
+            1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p), 
+            1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) );
         printf( "Created = %d. Deleted = %d. Existing = %d.\n",
             p->nCreated, p->nDeleted, p->nCreated - p->nDeleted );
         return 0;
     }
     // count the number of nodes in the table
-    if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
+    if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) )
     {
         printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
-        printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", 
-            Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p),
-            Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) );
+        printf( "Entries = %d. And = %d. Xor = %d. Total = %d.\n", 
+            Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p), 
+            Aig_ManAndNum(p) + Aig_ManExorNum(p) );
 
         return 0;
     }
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 5681f689..aebe6c95 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -78,11 +78,6 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
     Aig_ManForEachPi( p, pObj, i )
         Aig_ObjSetTravIdCurrent( p, pObj );
-    // if there are latches, mark them
-    if ( Aig_ManLatchNum(p) > 0 )
-        Aig_ManForEachObj( p, pObj, i )
-            if ( Aig_ObjIsLatch(pObj) )
-                Aig_ObjSetTravIdCurrent( p, pObj );
     // go through the nodes
     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
     Aig_ManForEachObj( p, pObj, i )
@@ -93,6 +88,32 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Levelizes the nodes
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    int nLevels, i;
+    nLevels = Aig_ManLevelNum( p );
+    vLevels = Vec_VecStart( nLevels + 1 );
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        assert( (int)pObj->Level <= nLevels );
+        Vec_VecPush( vLevels, pObj->Level, pObj );
+    }
+    return vLevels;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects internal nodes in the DFS order.]
 
   Description []
@@ -130,7 +151,6 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
     Vec_Ptr_t * vNodes;
 //    Aig_Obj_t * pObj;
     int i;
-    assert( Aig_ManLatchNum(p) == 0 );
     Aig_ManIncrementTravId( p );
     // mark constant and PIs
     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
@@ -245,11 +265,6 @@ Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p )
     // mark POs
     Aig_ManForEachPo( p, pObj, i )
         Aig_ObjSetTravIdCurrent( p, pObj );
-    // if there are latches, mark them
-    if ( Aig_ManLatchNum(p) > 0 )
-        Aig_ManForEachObj( p, pObj, i )
-            if ( Aig_ObjIsLatch(pObj) )
-                Aig_ObjSetTravIdCurrent( p, pObj );
     // go through the nodes
     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
     Aig_ManForEachObj( p, pObj, i )
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 665401c3..95bacf8a 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -102,6 +102,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     return pNew;
 }
 
+//#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG manager recursively.]
@@ -122,7 +124,7 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsBuf(pObj) )
         return pObj->pData = Aig_ObjChild0Copy(pObj);
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
     Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     return pObj->pData = pObjNew;
 }
@@ -148,7 +150,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->nRegs = p->nRegs;
     pNew->nAsserts = p->nAsserts;
-    pNew->pManHaig = p->pManHaig;  
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -164,7 +165,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
             }
             else if ( Aig_ObjIsNode(pObj) )
             {
-                pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+                pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
             }
             else if ( Aig_ObjIsPi(pObj) )
             {
@@ -187,6 +188,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     }
     else
     {
+/*
+
         Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
         Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
         Aig_ManForEachObj( p, pObj, i )
@@ -207,13 +210,73 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
                 pObj->pData = pObjNew;
             }
         }
+*/
+        Vec_Vec_t * vLevels;
+        int k;
+
+        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+        Aig_ManForEachPi( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->pHaig = pObj->pHaig;
+            pObjNew->Level = pObj->Level;
+            pObj->pData = pObjNew;
+        }
+
+        vLevels = Aig_ManLevelize( p );
+        Vec_VecForEachEntry( vLevels, pObj, i, k )
+        {
+            pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+        Vec_VecFree( vLevels );
+
+        // add the POs
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+            pObjNew->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+
+
+/*
+        Aig_ManForEachObj( p, pObj, i )
+        {
+            if ( Aig_ObjIsPi(pObj) )
+            {
+                pObjNew = Aig_ObjCreatePi( pNew );
+                pObjNew->Level = pObj->Level;
+            }
+            else if ( Aig_ObjIsPo(pObj) )
+            {
+//                pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+            }
+            else if ( Aig_ObjIsConst1(pObj) )
+            {
+                pObjNew = Aig_ManConst1(pNew);
+            }
+            else 
+            {
+                pObjNew = Aig_ManDup_rec( pNew, p, pObj );        
+            }
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+        // add the POs
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+            pObjNew->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+*/
     }
     // add the POs
-    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-    // pass the HAIG to the new AIG
-    p->pManHaig = NULL;
-    Aig_ManForEachObj( p, pObj, i )
-        pObj->pHaig = NULL;
+//    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
@@ -223,6 +286,117 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     return pNew;
 }
 
+//#endif
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew;
+    if ( pObj->pData )
+        return pObj->pData;
+    Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    if ( Aig_ObjIsBuf(pObj) )
+        return pObj->pData = Aig_ObjChild0Copy(pObj);
+    Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObjNew->pHaig = pObj->pHaig;
+        pObjNew->Level = pObj->Level;
+        pObj->pData = pObjNew;
+    }
+    // duplicate internal nodes
+    if ( fOrdered )
+    {
+        Aig_ManForEachObj( p, pObj, i )
+            if ( Aig_ObjIsBuf(pObj) )
+            {
+                pObj->pData = Aig_ObjChild0Copy(pObj);
+            }
+            else if ( Aig_ObjIsNode(pObj) )
+            {
+                pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+            }
+    }
+    else
+    {
+        Aig_ManForEachObj( p, pObj, i )
+            if ( !Aig_ObjIsPo(pObj) )
+            {
+                Aig_ManDup_rec( pNew, p, pObj );        
+                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+            }
+    }
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+/*
+    printf( "PIs : " );
+    Aig_ManForEachPi( p, pObj, i )
+        printf( "%d ", pObj->Id );
+    printf( "\n" );
+    printf( "PIs : " );
+    Aig_ManForEachPo( p, pObj, i )
+        printf( "%d ", pObj->Id );
+    printf( "\n" );
+*/
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDup(): The check has failed.\n" );
+    return pNew;
+}
+
+#endif
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG manager.]
@@ -252,7 +426,7 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
     {
         assert( !Aig_ObjIsBuf(pObj) );
         if ( Aig_ObjIsNode(pObj) )
-            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
     }
     return pNew;
 }
@@ -311,8 +485,6 @@ void Aig_ManStop( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
-    if ( p->pManHaig )
-        Aig_ManStop( p->pManHaig );
     if ( p->vMapped )
         Vec_PtrFree( p->vMapped );
     // print time
@@ -412,7 +584,7 @@ int Aig_ManHaigCounter( Aig_Man_t * pAig )
 void Aig_ManPrintStats( Aig_Man_t * p )
 {
     int nChoices = Aig_ManCountChoices(p);
-    printf( "PI/PO/Lat = %5d/%5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
+    printf( "PI/PO = %5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p) );
     printf( "A = %7d. ",   Aig_ManAndNum(p) );
     printf( "Eq = %7d. ",  Aig_ManHaigCounter(p) );
     if ( nChoices )
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 734f1277..2f92f720 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -88,7 +88,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     Aig_Obj_t * pObj;
     assert( !Aig_IsComplement(pGhost) );
     assert( Aig_ObjIsHash(pGhost) );
-//    assert( pGhost == &p->Ghost );
+    assert( pGhost == &p->Ghost );
     // get memory for the new object
     pObj = Aig_ManFetchMemory( p );
     pObj->Type = pGhost->Type;
@@ -97,14 +97,6 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Aig_ObjType(pObj)]++;
     assert( pObj->pData == NULL );
-/*
-    if ( p->pManHaig )
-    {
-        pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
-        pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
-        pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
-    }
-*/
     return pObj;
 }
 
@@ -374,13 +366,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     // make sure object is not pointing to itself
     assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
     assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
-    // map the HAIG nodes
-    if ( p->pManHaig != NULL )
-    {
-        assert( pObjNewR->pHaig != NULL );
-        assert( pObjNewR->pHaig->pHaig == NULL );
-        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
-    }
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
     Aig_ObjDelete_rec( p, pObjOld, 0 );
diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c
index c19f551e..6e9d37ba 100644
--- a/src/aig/aig/aigOper.c
+++ b/src/aig/aig/aigOper.c
@@ -89,43 +89,6 @@ Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the canonical form of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
-{
-    Aig_Obj_t * pResult, * pLat0, * pLat1;
-    int fCompl0, fCompl1;
-    Aig_Type_t Type;
-    assert( Aig_ObjIsNode(pGhost) );
-    // consider the case when the pair is canonical
-    if ( !Aig_ObjIsLatch(Aig_ObjFanin0(pGhost)) || !Aig_ObjIsLatch(Aig_ObjFanin1(pGhost)) )
-    {
-        if ( (pResult = Aig_TableLookup( p, pGhost )) )
-            return pResult;
-        return Aig_ObjCreate( p, pGhost );
-    }
-    /// remember the latches
-    pLat0 = Aig_ObjFanin0(pGhost);
-    pLat1 = Aig_ObjFanin1(pGhost);
-    // remember type and compls
-    Type = Aig_ObjType(pGhost);
-    fCompl0 = Aig_ObjFaninC0(pGhost);
-    fCompl1 = Aig_ObjFaninC1(pGhost);
-    // call recursively
-    pResult = Aig_Oper( p, Aig_NotCond(Aig_ObjChild0(pLat0), fCompl0), Aig_NotCond(Aig_ObjChild0(pLat1), fCompl1), Type );
-    // build latch on top of this
-    return Aig_Latch( p, pResult, (Type == AIG_OBJ_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Performs canonicization step.]
 
   Description [The argument nodes can be complemented.]
@@ -138,16 +101,7 @@ Aig_Obj_t * Aig_CanonPair_rec( Aig_Man_t * p, Aig_Obj_t * pGhost )
 Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 {
     Aig_Obj_t * pGhost, * pResult;
-//    Aig_Obj_t * pFan0, * pFan1;
-    if ( p->pTable == NULL )
-    {
-//        pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
-        pGhost = Aig_ManGhost(p);
-        pGhost->Type = AIG_OBJ_AND;
-        pGhost->pFanin0 = p0;
-        pGhost->pFanin1 = p1;
-        return Aig_ObjCreate( p, pGhost );
-    }
+    Aig_Obj_t * pFan0, * pFan1;
     // check trivial cases
     if ( p0 == p1 )
         return p0;
@@ -241,32 +195,12 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
         }
     }
     // check if it can be an EXOR gate
-//    if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
-//        return Aig_Exor( p, pFan0, pFan1 );
+    if ( p->fCatchExor && Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
+        return Aig_Exor( p, pFan0, pFan1 );
     pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_AND );
-    pResult = Aig_CanonPair_rec( p, pGhost );
-    return pResult;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the canonical form of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
-{
-    Aig_Obj_t * pGhost, * pResult;
-    pGhost = Aig_ObjCreateGhost( p, Aig_NotCond(pObj, fInitOne), NULL, AIG_OBJ_LATCH );
-    pResult = Aig_TableLookup( p, pGhost );
-    if ( pResult == NULL )
-        pResult = Aig_ObjCreate( p, pGhost );
-    return Aig_NotCond( pResult, fInitOne );
+    if ( (pResult = Aig_TableLookup( p, pGhost )) )
+        return pResult;
+    return Aig_ObjCreate( p, pGhost );
 }
 
 /**Function*************************************************************
@@ -282,8 +216,8 @@ Aig_Obj_t * Aig_Latch( Aig_Man_t * p, Aig_Obj_t * pObj, int fInitOne )
 ***********************************************************************/
 Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 {
-/*
     Aig_Obj_t * pGhost, * pResult;
+    int fCompl;
     // check trivial cases
     if ( p0 == p1 )
         return Aig_Not(p->pConst1);
@@ -293,13 +227,19 @@ Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
         return Aig_NotCond( p1, p0 == p->pConst1 );
     if ( Aig_Regular(p1) == p->pConst1 )
         return Aig_NotCond( p0, p1 == p->pConst1 );
-    // check the table
+    // when there is no special XOR gates
+    if ( !p->fCatchExor )
+        return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
+    // canonicize
+    fCompl = Aig_IsComplement(p0) ^ Aig_IsComplement(p1);
+    p0 = Aig_Regular(p0);
+    p1 = Aig_Regular(p1);
     pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_OBJ_EXOR );
+    // check the table
     if ( pResult = Aig_TableLookup( p, pGhost ) )
-        return pResult;
-    return Aig_ObjCreate( p, pGhost );
-*/
-    return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
+        return Aig_NotCond( pResult, fCompl );
+    pResult = Aig_ObjCreate( p, pGhost );
+    return Aig_NotCond( pResult, fCompl );
 }
 
 /**Function*************************************************************
@@ -331,7 +271,7 @@ Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 ***********************************************************************/
 Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
 {
-/*    
+/*
     Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
     int Count0, Count1;
     // consider trivial cases
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index 4318be9d..e52283b1 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -178,18 +178,6 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
             p->nObjs[AIG_OBJ_BUF]++;
             Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
             // create HAIG if defined
-/*
-            if ( p->pManHaig )
-            {
-                // create HAIG latch
-                pObjLo->pHaig = Aig_ObjCreatePi( p->pManHaig );
-                pObjLi->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( Aig_ObjChild0(pObjLi) ) );
-                // create equivalence class
-                assert( pObjLo->pHaig != NULL );
-                assert( pObjLo->pHaig->pHaig == NULL );
-                pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
-            }
-*/
             // mark the change
             fChange = 1;
             // check the limit
diff --git a/src/aig/aig/aigSeq.c b/src/aig/aig/aigSeq.c
deleted file mode 100644
index daafeab1..00000000
--- a/src/aig/aig/aigSeq.c
+++ /dev/null
@@ -1,502 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigSeq.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [AIG package.]
-
-  Synopsis    [Sequential strashing.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - April 28, 2007.]
-
-  Revision    [$Id: aigSeq.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Converts combinational AIG manager into a sequential one.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManSeqStrashConvert( Aig_Man_t * p, int nLatches, int * pInits )
-{
-    Aig_Obj_t * pObjLi, * pObjLo, * pLatch;
-    int i;
-    assert( Vec_PtrSize( p->vBufs ) == 0 );
-    // collect the POs to be converted into latches
-    for ( i = 0; i < nLatches; i++ )
-    {
-        // get the corresponding PI/PO pair
-        pObjLi = Aig_ManPo( p, Aig_ManPoNum(p) - nLatches + i );
-        pObjLo = Aig_ManPi( p, Aig_ManPiNum(p) - nLatches + i );
-        // create latch
-        pLatch = Aig_Latch( p, Aig_ObjChild0(pObjLi), pInits? pInits[i] : 0 );
-        // recycle the old PO object
-        Aig_ObjDisconnect( p, pObjLi );
-        Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL );
-        Aig_ManRecycleMemory( p, pObjLi );
-        // convert the corresponding PI to be a buffer and connect it to the latch
-        pObjLo->Type = AIG_OBJ_BUF;
-        Aig_ObjConnect( p, pObjLo, pLatch, NULL );
-        // save the buffer
-//        Vec_PtrPush( p->vBufs, pObjLo );
-    }
-    // shrink the arrays
-    Vec_PtrShrink( p->vPis, Aig_ManPiNum(p) - nLatches );
-    Vec_PtrShrink( p->vPos, Aig_ManPoNum(p) - nLatches );
-    // update the counters of different objects
-    p->nObjs[AIG_OBJ_PI]  -= nLatches;
-    p->nObjs[AIG_OBJ_PO]  -= nLatches;
-    p->nObjs[AIG_OBJ_BUF] += nLatches;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDfsSeq_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( pObj == NULL )
-        return;
-    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
-        return;
-    Aig_ObjSetTravIdCurrent( p, pObj );
-    if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
-        return;
-    Aig_ManDfsSeq_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    Aig_ManDfsSeq_rec( p, Aig_ObjFanin1(pObj), vNodes );
-//    if ( (Aig_ObjFanin0(pObj) == NULL || Aig_ObjIsBuf(Aig_ObjFanin0(pObj))) &&
-//         (Aig_ObjFanin1(pObj) == NULL || Aig_ObjIsBuf(Aig_ObjFanin1(pObj))) )
-        Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsSeq( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManIncrementTravId( p );
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ManDfsSeq_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDfsUnreach_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( pObj == NULL )
-        return;
-    if ( Aig_ObjIsTravIdPrevious(p, pObj) || Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdPrevious( p, pObj ); // assume unknown
-    Aig_ManDfsUnreach_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    Aig_ManDfsUnreach_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    if ( Aig_ObjIsTravIdPrevious(p, Aig_ObjFanin0(pObj)) && 
-        (Aig_ObjFanin1(pObj) == NULL || Aig_ObjIsTravIdPrevious(p, Aig_ObjFanin1(pObj))) )
-        Vec_PtrPush( vNodes, pObj );
-    else
-        Aig_ObjSetTravIdCurrent( p, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes unreachable from PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsUnreach( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj, * pFanin;
-    int i, k;//, RetValue;
-    // collect unreachable nodes
-    Aig_ManIncrementTravId( p ); 
-    Aig_ManIncrementTravId( p ); 
-    // mark the constant and PIs
-    Aig_ObjSetTravIdPrevious( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    // curr marks visited nodes reachable from PIs
-    // prev marks visited nodes unreachable or unknown
-
-    // collect the unreachable nodes
-    vNodes = Vec_PtrAlloc( 32 );
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ManDfsUnreach_rec( p, Aig_ObjFanin0(pObj), vNodes );
-
-    // refine resulting nodes
-    do 
-    {
-        k = 0;
-        Vec_PtrForEachEntry( vNodes, pObj, i )
-        {
-            assert( Aig_ObjIsTravIdPrevious(p, pObj) );
-            if ( Aig_ObjIsLatch(pObj) || Aig_ObjIsBuf(pObj) )
-            {
-                pFanin = Aig_ObjFanin0(pObj);
-                assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
-                if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
-                {
-                    Aig_ObjSetTravIdCurrent( p, pObj );
-                    continue;
-                }
-            }
-            else // AND gate
-            {
-                assert( Aig_ObjIsNode(pObj) );
-                pFanin = Aig_ObjFanin0(pObj);
-                assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
-                if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
-                {
-                    Aig_ObjSetTravIdCurrent( p, pObj );
-                    continue;
-                }
-                pFanin = Aig_ObjFanin1(pObj);
-                assert( Aig_ObjIsTravIdPrevious(p, pFanin) || Aig_ObjIsTravIdCurrent(p, pFanin) );
-                if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
-                {
-                    Aig_ObjSetTravIdCurrent( p, pObj );
-                    continue;
-                }
-            }
-            // write it back
-            Vec_PtrWriteEntry( vNodes, k++, pObj );
-        }
-        Vec_PtrShrink( vNodes, k );
-    } 
-    while ( k < i );
-
-//    if ( Vec_PtrSize(vNodes) > 0 )
-//        printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) ); 
-    return vNodes;
-
-/*
-    // the resulting array contains all unreachable nodes except const 1
-    if ( Vec_PtrSize(vNodes) == 0 )
-    {
-        Vec_PtrFree( vNodes );
-        return 0;
-    }
-    RetValue = Vec_PtrSize(vNodes);
-
-    // mark these nodes
-    Aig_ManIncrementTravId( p ); 
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-    Vec_PtrFree( vNodes );
-    return RetValue;
-*/
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Removes nodes that do not fanout into POs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManRemoveUnmarked( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i, RetValue;
-    // collect unmarked nodes
-    vNodes = Vec_PtrAlloc( 100 );
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( Aig_ObjIsTerm(pObj) )
-            continue;
-        if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-            continue;
-//Aig_ObjPrintVerbose( pObj, 0 );
-        Aig_ObjDisconnect( p, pObj );
-        Vec_PtrPush( vNodes, pObj );
-    }
-    if ( Vec_PtrSize(vNodes) == 0 )
-    {
-        Vec_PtrFree( vNodes );
-        return 0;
-    }
-    // remove the dangling objects
-    RetValue = Vec_PtrSize(vNodes);
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Aig_ObjDelete( p, pObj );
-//    printf( "Removed %d dangling.\n", Vec_PtrSize(vNodes) ); 
-    Vec_PtrFree( vNodes );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Rehashes the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManSeqRehashOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach )
-{
-    Aig_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
-    int i, RetValue = 0, Counter = 0;//, Counter2 = 0;
-
-    // mark the unreachable nodes
-    Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vUnreach, pObj, i )
-        Aig_ObjSetTravIdCurrent(p, pObj);
-/*
-    // count the number of unreachable object connections
-    // that is the number of unreachable objects connected to main objects
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-            continue;
-
-        pFanin0 = Aig_ObjFanin0(pObj);
-        if ( pFanin0 == NULL )
-            continue;
-        if ( Aig_ObjIsTravIdCurrent(p, pFanin0) )
-            pFanin0->fMarkA = 1;
-
-        pFanin1 = Aig_ObjFanin1(pObj);
-        if ( pFanin1 == NULL )
-            continue;
-        if ( Aig_ObjIsTravIdCurrent(p, pFanin1) )
-            pFanin1->fMarkA = 1;
-    }
-
-    // count the objects
-    Aig_ManForEachObj( p, pObj, i )
-        Counter2 += pObj->fMarkA, pObj->fMarkA = 0;
-    printf( "Connections = %d.\n", Counter2 );
-*/
-
-    // go through the nodes while skipping unreachable
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        // skip nodes unreachable from the PIs
-        if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-            continue;
-        // process the node
-        if ( Aig_ObjIsPo(pObj) )
-        {
-            if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
-                continue;
-            pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            Aig_ObjPatchFanin0( p, pObj, pFanin0 );
-            continue;
-        }
-        if ( Aig_ObjIsLatch(pObj) )
-        {
-            if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
-                continue;
-            pObjNew = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pObjNew = Aig_Latch( p, pObjNew, 0 );
-            Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
-            RetValue = 1;
-            Counter++;
-            continue;
-        }
-        if ( Aig_ObjIsNode(pObj) )
-        {
-            if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) && !Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) )
-                continue;
-            pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
-            pObjNew = Aig_And( p, pFanin0, pFanin1 );
-            Aig_ObjReplace( p, pObj, pObjNew, 1, 0 );
-            RetValue = 1;
-            Counter++;
-            continue;
-        }
-    }
-//    printf( "Rehashings = %d.\n", Counter++ );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [If AIG contains buffers, this procedure removes them.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManRemoveBuffers( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
-    int i;
-    if ( Aig_ManBufNum(p) == 0 )
-        return;
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( Aig_ObjIsPo(pObj) )
-        {
-            if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
-                continue;
-            pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            Aig_ObjPatchFanin0( p, pObj, pFanin0 );
-        }
-        else if ( Aig_ObjIsLatch(pObj) )
-        {
-            if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) )
-                continue;
-            pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pObjNew = Aig_Latch( p, pFanin0, 0 );
-            Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
-        }
-        else if ( Aig_ObjIsAnd(pObj) )
-        {
-            if ( !Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) && !Aig_ObjIsBuf(Aig_ObjFanin1(pObj)) )
-                continue;
-            pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
-            pObjNew = Aig_And( p, pFanin0, pFanin1 );
-            Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
-        }
-    }
-    assert( Aig_ManBufNum(p) == 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits )
-{
-    Vec_Ptr_t * vNodes, * vUnreach;
-//    Aig_Obj_t * pObj, * pFanin;
-//    int i;
-    int Iter, RetValue = 1;
-
-    // create latches out of the additional PI/PO pairs
-    Aig_ManSeqStrashConvert( p, nLatches, pInits );
-
-    // iteratively rehash the network
-    for ( Iter = 0; RetValue; Iter++ )
-    {
-//        Aig_ManPrintStats( p );
-/*
-        Aig_ManForEachObj( p, pObj, i )
-        {
-            assert( pObj->Type > 0 );
-            pFanin = Aig_ObjFanin0(pObj);
-            assert( pFanin == NULL || pFanin->Type > 0 );
-            pFanin = Aig_ObjFanin1(pObj);
-            assert( pFanin == NULL || pFanin->Type > 0 );
-        }
-*/
-        // mark nodes unreachable from the PIs
-        vUnreach = Aig_ManDfsUnreach( p );
-        if ( Iter == 0 && Vec_PtrSize(vUnreach) > 0 )
-            printf( "Unreachable objects = %d.\n", Vec_PtrSize(vUnreach) );
-        // collect nodes reachable from the POs
-        vNodes = Aig_ManDfsSeq( p );
-        // remove nodes unreachable from the POs
-        if ( Iter == 0 )
-            Aig_ManRemoveUnmarked( p );
-        // continue rehashing as long as there are changes
-        RetValue = Aig_ManSeqRehashOne( p, vNodes, vUnreach );
-        Vec_PtrFree( vNodes );
-        Vec_PtrFree( vUnreach );
-    }
-
-    // perform the final cleanup
-    Aig_ManIncrementTravId( p );
-    vNodes = Aig_ManDfsSeq( p );
-    Aig_ManRemoveUnmarked( p );
-    Vec_PtrFree( vNodes );
-    // remove buffers if they are left
-//    Aig_ManRemoveBuffers( p );
-
-    // clean up
-    if ( !Aig_ManCheck( p ) )
-    {
-        printf( "Aig_ManSeqStrash: The network check has failed.\n" );
-        return 0;
-    }
-    return 1;
-
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/aig/aigShow.c b/src/aig/aig/aigShow.c
index 96b0e37f..8dc67c79 100644
--- a/src/aig/aig/aigShow.c
+++ b/src/aig/aig/aigShow.c
@@ -170,7 +170,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
 */
         fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id ); 
 
-        fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"invtriangle") );
+        fprintf( pFile, ", shape = %s", "invtriangle" );
         fprintf( pFile, ", color = coral, fillcolor = coral" );
         fprintf( pFile, "];\n" );
     }
@@ -237,7 +237,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
 */
         fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id ); 
 
-        fprintf( pFile, ", shape = %s", (Aig_ObjIsLatch(pNode)? "box":"triangle") );
+        fprintf( pFile, ", shape = %s", "triangle" );
         fprintf( pFile, ", color = coral, fillcolor = coral" );
         fprintf( pFile, "];\n" );
     }
@@ -248,7 +248,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
     // generate invisible edges from the square down
     fprintf( pFile, "title1 -> title2 [style = invis];\n" );
     Aig_ManForEachPo( pMan, pNode, i )
-        fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") );
+        fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
 
     // generate edges
     Aig_ManForEachObj( pMan, pNode, i )
@@ -256,9 +256,9 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
         if ( !Aig_ObjIsNode(pNode) && !Aig_ObjIsPo(pNode) && !Aig_ObjIsBuf(pNode) )
             continue;
         // generate the edge from this node to the next
-        fprintf( pFile, "Node%d%s",  pNode->Id, (Aig_ObjIsLatch(pNode)? "_in":"") );
+        fprintf( pFile, "Node%d",  pNode->Id );
         fprintf( pFile, " -> " );
-        fprintf( pFile, "Node%d%s",  Aig_ObjFaninId0(pNode), (Aig_ObjIsLatch(Aig_ObjFanin0(pNode))? "_out":"") );
+        fprintf( pFile, "Node%d",  Aig_ObjFaninId0(pNode) );
         fprintf( pFile, " [" );
         fprintf( pFile, "style = %s", Aig_ObjFaninC0(pNode)? "dotted" : "bold" );
 //        if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 )
@@ -270,7 +270,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
         // generate the edge from this node to the next
         fprintf( pFile, "Node%d",  pNode->Id );
         fprintf( pFile, " -> " );
-        fprintf( pFile, "Node%d%s",  Aig_ObjFaninId1(pNode), (Aig_ObjIsLatch(Aig_ObjFanin1(pNode))? "_out":"") );
+        fprintf( pFile, "Node%d",  Aig_ObjFaninId1(pNode) );
         fprintf( pFile, " [" );
         fprintf( pFile, "style = %s", Aig_ObjFaninC1(pNode)? "dotted" : "bold" );
 //        if ( Aig_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 )
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 357b63c3..9cfbf5f2 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -39,15 +39,8 @@ static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize )
 static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t ** ppEntry;
-    if ( Aig_ObjIsLatch(pObj) )
-    {
-        assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) == NULL );
-    }
-    else
-    {
-        assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
-        assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id );
-    }
+    assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
+    assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id );
     for ( ppEntry = p->pTable + Aig_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
         if ( *ppEntry == pObj )
             return ppEntry;
@@ -119,20 +112,11 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
 {
     Aig_Obj_t * pEntry;
     assert( !Aig_IsComplement(pGhost) );
-    if ( pGhost->Type == AIG_OBJ_LATCH )
-    {
-        assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) == NULL );
-        if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) )
-            return NULL;
-    }
-    else
-    {
-        assert( pGhost->Type == AIG_OBJ_AND );
-        assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
-        assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
-        if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
-            return NULL;
-    }
+    assert( Aig_ObjIsNode(pGhost) );
+    assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
+    assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
+    if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
+        return NULL;
     for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
     {
         if ( Aig_ObjChild0(pEntry) == Aig_ObjChild0(pGhost) && 
@@ -184,8 +168,6 @@ Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t *
 void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t ** ppPlace;
-    if ( p->pTable == NULL )
-        return;
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_TableLookup(p, pObj) == NULL );
     if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) )
@@ -209,8 +191,6 @@ void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
 void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t ** ppPlace;
-    if ( p->pTable == NULL )
-        return;
     assert( !Aig_IsComplement(pObj) );
     ppPlace = Aig_TableFind( p, pObj );
     assert( *ppPlace == pObj ); // node should be in the table
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 00a85c26..ddb12e6e 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -16,7 +16,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigRet.c \
     src/aig/aig/aigRetF.c \
     src/aig/aig/aigScl.c \
-    src/aig/aig/aigSeq.c \
     src/aig/aig/aigShow.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 03707481..63f6f232 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -25,151 +25,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
-static Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
-static int         Dar_BalanceFindLeft( Vec_Ptr_t * vSuper );
-static void        Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
-static void        Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj );
-static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs algebraic balancing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pDriver, * pObjNew;
-    Vec_Vec_t * vStore;
-    int i;
-    // create the new manager 
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->nRegs = p->nRegs;
-    pNew->nAsserts = p->nAsserts;
-    if ( p->vFlopNums )
-        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
-    // map the PI nodes
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    vStore = Vec_VecAlloc( 50 );
-    if ( p->pManTime != NULL )
-    {
-        float arrTime;
-        Tim_ManIncrementTravId( p->pManTime );
-        Aig_ManSetPioNumbers( p );
-        Aig_ManForEachObj( p, pObj, i )
-        {
-            if ( Aig_ObjIsAnd(pObj) || Aig_ObjIsConst1(pObj) )
-                continue;
-            if ( Aig_ObjIsPi(pObj) )
-            {
-                // copy the PI
-                pObjNew = Aig_ObjCreatePi(pNew); 
-                pObj->pData = pObjNew;
-                // set the arrival time of the new PI
-                arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
-                pObjNew->Level = (int)arrTime;
-            }
-            else if ( Aig_ObjIsPo(pObj) )
-            {
-                // perform balancing
-                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
-                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-                Aig_ObjCreatePo( pNew, pObjNew );
-                // save arrival time of the output
-                arrTime = (float)Aig_Regular(pObjNew)->Level;
-                Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
-            }
-            else
-                assert( 0 );
-        }
-        Aig_ManCleanPioNumbers( p );
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
-    }
-    else
-    {
-        Aig_ManForEachPi( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePi(pNew); 
-            pObjNew->Level = pObj->Level;
-            pObj->pData = pObjNew;
-        }
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
-            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
-            pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-            Aig_ObjCreatePo( pNew, pObjNew );
-        }
-    }
-    Vec_VecFree( vStore );
-    // remove dangling nodes
-    Aig_ManCleanup( pNew );
-    // check the resulting AIG
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Dar_ManBalance(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the new node constructed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
-{
-    Aig_Obj_t * pObjNew;
-    Vec_Ptr_t * vSuper;
-    int i;
-    assert( !Aig_IsComplement(pObjOld) );
-    assert( !Aig_ObjIsBuf(pObjOld) );
-    // return if the result is known
-    if ( pObjOld->pData )
-        return pObjOld->pData;
-    assert( Aig_ObjIsNode(pObjOld) );
-    // get the implication supergate
-    vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
-    // check if supergate contains two nodes in the opposite polarity
-    if ( vSuper->nSize == 0 )
-        return pObjOld->pData = Aig_ManConst0(pNew);
-    if ( Vec_PtrSize(vSuper) < 2 )
-        printf( "BUG!\n" );
-    // for each old node, derive the new well-balanced node
-    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
-    {
-        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
-        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
-    }
-    // build the supergate
-    pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
-    // make sure the balanced node is not assigned
-//    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
-    assert( pObjOld->pData == NULL );
-    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
-    return pObjOld->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Collects the nodes of the supergate.]
 
   Description []
@@ -185,14 +46,26 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
     // check if the node is visited
     if ( Aig_Regular(pObj)->fMarkB )
     {
-        // check if the node occurs in the same polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == pObj )
-                return 1;
-        // check if the node is present in the opposite polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == Aig_Not(pObj) )
-                return -1;
+        if ( Aig_ObjIsExor(pRoot) )
+        {
+            assert( !Aig_IsComplement(pObj) );
+            // check if the node occurs in the same polarity
+            Vec_PtrRemove( vSuper, pObj );
+            Aig_Regular(pObj)->fMarkB = 0;
+//printf( " Duplicated EXOR input!!! " );
+            return 1;
+        }
+        else
+        {
+            // check if the node occurs in the same polarity
+            for ( i = 0; i < vSuper->nSize; i++ )
+                if ( vSuper->pArray[i] == pObj )
+                    return 1;
+            // check if the node is present in the opposite polarity
+            for ( i = 0; i < vSuper->nSize; i++ )
+                if ( vSuper->pArray[i] == Aig_Not(pObj) )
+                    return -1;
+        }
         assert( 0 );
         return 0;
     }
@@ -251,60 +124,6 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
-{
-    int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
-    if ( Diff > 0 )
-        return -1;
-    if ( Diff < 0 ) 
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Builds implication supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
-{
-    Aig_Obj_t * pObj1, * pObj2;
-    int LeftBound;
-    assert( vSuper->nSize > 1 );
-    // sort the new nodes by level in the decreasing order
-    Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
-    // balance the nodes
-    while ( vSuper->nSize > 1 )
-    {
-        // find the left bound on the node to be paired
-        LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
-        // find the node that can be shared (if no such node, randomize choice)
-        Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
-        // pull out the last two nodes
-        pObj1 = Vec_PtrPop(vSuper);
-        pObj2 = Vec_PtrPop(vSuper);
-        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
-    }
-    return Vec_PtrEntry(vSuper, 0);
-}
-
-/**Function*************************************************************
-
   Synopsis    [Finds the left bound on the next candidate to be paired.]
 
   Description [The nodes in the array are in the decreasing order of levels. 
@@ -405,6 +224,27 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+    int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
   Synopsis    [Inserts a new node in the order by levels.]
 
   Description []
@@ -432,6 +272,220 @@ void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Builds implication supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
+{
+    Aig_Obj_t * pObj1, * pObj2;
+    int LeftBound;
+    assert( vSuper->nSize > 1 );
+    // sort the new nodes by level in the decreasing order
+    Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
+    // balance the nodes
+    while ( vSuper->nSize > 1 )
+    {
+        // find the left bound on the node to be paired
+        LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper );
+        // find the node that can be shared (if no such node, randomize choice)
+        Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
+        // pull out the last two nodes
+        pObj1 = Vec_PtrPop(vSuper);
+        pObj2 = Vec_PtrPop(vSuper);
+        Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
+    }
+    return Vec_PtrEntry(vSuper, 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the new node constructed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
+{
+    Aig_Obj_t * pObjNew;
+    Vec_Ptr_t * vSuper;
+    int i;
+    assert( !Aig_IsComplement(pObjOld) );
+    assert( !Aig_ObjIsBuf(pObjOld) );
+    // return if the result is known
+    if ( pObjOld->pData )
+        return pObjOld->pData;
+    assert( Aig_ObjIsNode(pObjOld) );
+    // get the implication supergate
+    vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
+    // check if supergate contains two nodes in the opposite polarity
+    if ( vSuper->nSize == 0 )
+        return pObjOld->pData = Aig_ManConst0(pNew);
+    if ( Vec_PtrSize(vSuper) < 2 )
+        printf( "BUG!\n" );
+    // for each old node, derive the new well-balanced node
+    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
+    {
+        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
+    }
+    // build the supergate
+    pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
+    // make sure the balanced node is not assigned
+//    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
+    assert( pObjOld->pData == NULL );
+    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
+    return pObjOld->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs algebraic balancing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pDriver, * pObjNew;
+    Vec_Vec_t * vStore;
+    int i;
+    // create the new manager 
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // map the PI nodes
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    vStore = Vec_VecAlloc( 50 );
+    if ( p->pManTime != NULL )
+    {
+        float arrTime;
+        Tim_ManIncrementTravId( p->pManTime );
+        Aig_ManSetPioNumbers( p );
+        Aig_ManForEachObj( p, pObj, i )
+        {
+            if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
+                continue;
+            if ( Aig_ObjIsPi(pObj) )
+            {
+                // copy the PI
+                pObjNew = Aig_ObjCreatePi(pNew); 
+                pObj->pData = pObjNew;
+                // set the arrival time of the new PI
+                arrTime = Tim_ManGetPiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
+                pObjNew->Level = (int)arrTime;
+            }
+            else if ( Aig_ObjIsPo(pObj) )
+            {
+                // perform balancing
+                pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+                pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+                pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+                Aig_ObjCreatePo( pNew, pObjNew );
+                // save arrival time of the output
+                arrTime = (float)Aig_Regular(pObjNew)->Level;
+                Tim_ManSetPoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+            }
+            else
+                assert( 0 );
+        }
+        Aig_ManCleanPioNumbers( p );
+        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    }
+    else
+    {
+        Aig_ManForEachPi( p, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePi(pNew); 
+            pObjNew->Level = pObj->Level;
+            pObj->pData = pObjNew;
+        }
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+            pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+            pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+            Aig_ObjCreatePo( pNew, pObjNew );
+        }
+    }
+    Vec_VecFree( vStore );
+    // remove dangling nodes
+    Aig_ManCleanup( pNew );
+    // check the resulting AIG
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Dar_ManBalance(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts a new node in the order by levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_BalancePrintStats( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vSuper;
+    Aig_Obj_t * pObj, * pTemp;
+    int i, k;
+    if ( Aig_ManExorNum(p) == 0 )
+    {
+        printf( "There is no EXOR gates.\n" );
+        return;
+    }
+    Aig_ManForEachExor( p, pObj, i )
+    {
+        Aig_ObjFanin0(pObj)->fMarkA = 1;
+        Aig_ObjFanin1(pObj)->fMarkA = 1;
+        assert( !Aig_ObjFaninC0(pObj) );
+        assert( !Aig_ObjFaninC1(pObj) );
+    }
+    vSuper = Vec_PtrAlloc( 1000 );
+    Aig_ManForEachExor( p, pObj, i )
+    {
+        if ( pObj->fMarkA && pObj->nRefs == 1 )
+            continue;
+        Vec_PtrClear( vSuper );
+        Dar_BalanceCone_rec( pObj, pObj, vSuper );
+        Vec_PtrForEachEntry( vSuper, pTemp, k )
+            pTemp->fMarkB = 0;
+        if ( Vec_PtrSize(vSuper) < 3 )
+            continue;
+        printf( "  %d(", Vec_PtrSize(vSuper) );
+        Vec_PtrForEachEntry( vSuper, pTemp, k )
+            printf( " %d", pTemp->Level );
+        printf( " )" );
+    }
+    Vec_PtrFree( vSuper );
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->fMarkA = 0;
+    printf( "\n" );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index a4ac9082..116b1591 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -201,14 +201,6 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
-    // balance
-    if ( fBalance )
-    {
-    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
-    Aig_ManStop( pTemp );
-    if ( fVerbose ) Aig_ManPrintStats( pAig );
-    }
-
     return pAig;
 }
 
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 67940c4f..444157f0 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -371,7 +371,6 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     if ( Aig_ManNodeNum(pManAig) == 0 )
         return Aig_ManDup(pManAig, 1);
 clk = clock();
-    assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
     p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 18c9ffcc..1ac2adab 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -344,7 +344,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
         pParams->nIters = 0;
         return Aig_ManDup(pManAig, 1);
     }
-    assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( pParams->nFramesK > 0 );
 //Aig_ManShow( pManAig, 0, NULL );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index a6460ed7..9149aca4 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -516,7 +516,6 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
         if ( pnIter ) *pnIter = 0;
         return Aig_ManDup(pAig, 1);
     }
-    assert( Aig_ManLatchNum(pAig) == 0 );
     assert( Aig_ManRegNum(pAig) > 0 );
 
     // simulate the AIG 
diff --git a/src/aig/hop/hopTruth.c b/src/aig/hop/hopTruth.c
index 9a2161b6..47358715 100644
--- a/src/aig/hop/hopTruth.c
+++ b/src/aig/hop/hopTruth.c
@@ -176,8 +176,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars
 //    assert( Hop_ManPiNum(p) <= 8 ); 
     if ( fMsbFirst )
     {
-        Hop_ManForEachPi( p, pObj, i )
+//        Hop_ManForEachPi( p, pObj, i )
+        for ( i = 0; i < nVars; i++ )
         {
+            pObj = Hop_ManPi( p, i );
             if ( vTtElems )
                 pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
             else               
@@ -186,8 +188,10 @@ unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars
     }
     else
     {
-        Hop_ManForEachPi( p, pObj, i )
+//        Hop_ManForEachPi( p, pObj, i )
+        for ( i = 0; i < nVars; i++ )
         {
+            pObj = Hop_ManPi( p, i );
             if ( vTtElems )
                 pObj->pData = Vec_PtrEntry(vTtElems, i);
             else               
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 65403609..c9626286 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2255,6 +2255,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     bool fDuplicate;
     bool fSelective;
     bool fUpdateLevel;
+    int fExor;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -2264,8 +2267,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     fDuplicate   = 0;
     fSelective   = 0;
     fUpdateLevel = 1;
+    fExor        = 0;
+    fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ldsh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ldsxvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2278,6 +2283,12 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fSelective ^= 1;
             break;
+        case 'x':
+            fExor ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2293,7 +2304,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective, fUpdateLevel );
+        if ( fExor ) 
+            pNtkRes = Abc_NtkBalanceExor( pNtk, fUpdateLevel, fVerbose );
+        else
+            pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective, fUpdateLevel );
     }
     else
     {
@@ -2303,7 +2317,10 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Strashing before balancing has failed.\n" );
             return 1;
         }
-        pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective, fUpdateLevel );
+        if ( fExor ) 
+            pNtkRes = Abc_NtkBalanceExor( pNtkTemp, fUpdateLevel, fVerbose );
+        else
+            pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective, fUpdateLevel );
         Abc_NtkDelete( pNtkTemp );
     }
 
@@ -2318,11 +2335,13 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: balance [-ldsh]\n" );
+    fprintf( pErr, "usage: balance [-ldsxvh]\n" );
     fprintf( pErr, "\t        transforms the current network into a well-balanced AIG\n" );
     fprintf( pErr, "\t-l    : toggle minimizing the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-d    : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" );
     fprintf( pErr, "\t-s    : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" );
+    fprintf( pErr, "\t-x    : toggle balancing multi-input EXORs [default = %s]\n", fExor? "yes": "no" );
+    fprintf( pErr, "\t-v    : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -7085,6 +7104,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
+//    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
+
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7269,7 +7290,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 //    Abc_NtkDarPartition( pNtk );
 /*
-    pNtkRes = Abc_NtkDarPartition( pNtk );
+    pNtkRes = Abc_NtkTestExor( pNtk, 0 );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -13363,7 +13384,6 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
     extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
-    extern void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -13453,9 +13473,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform equivalence checking
-    if ( fRetime )
-        Abc_NtkSecRetime( pNtk1, pNtk2 );
-    else if ( fSat )
+    if ( fSat )
         Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames );
     else
         Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dd8f8221..8f28a57f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -44,7 +44,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
+Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
 {
     Aig_Man_t * pMan;
     Aig_Obj_t * pObjNew;
@@ -90,6 +90,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
     }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+    pMan->fCatchExor = fExors;
+
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
     // save the number of registers
     if ( fRegisters )
@@ -127,7 +129,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
             if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
                 pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
     // remove dangling nodes
-    if ( nNodes = Aig_ManCleanup( pMan ) )
+    nNodes = Aig_ManCleanup( pMan );
+    if ( !fExors && nNodes )
         printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
 //Aig_ManDumpVerilog( pMan, "test.v" );
     if ( !Aig_ManCheck( pMan ) )
@@ -398,8 +401,6 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     // create latches of the new network
     Aig_ManForEachObj( pMan, pObj, i )
     {
-        if ( !Aig_ObjIsLatch(pObj) )
-            continue;
         pObjNew = Abc_NtkCreateLatch( pNtkNew );
         pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
         pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
@@ -435,8 +436,6 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     // connect the latches
     Aig_ManForEachObj( pMan, pObj, i )
     {
-        if ( !Aig_ObjIsLatch(pObj) )
-            continue;
         pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
         Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew );
     }
@@ -472,54 +471,6 @@ Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs verification after retiming.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
-{
-    int fRemove1, fRemove2;
-    Aig_Man_t * pMan1, * pMan2;
-    int * pArray;
-
-    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
-    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
-
-
-    pMan1 = Abc_NtkToDar( pNtk1, 0 );
-    pMan2 = Abc_NtkToDar( pNtk2, 0 );
-
-    Aig_ManPrintStats( pMan1 );
-    Aig_ManPrintStats( pMan2 );
-
-//    pArray = Abc_NtkGetLatchValues(pNtk1);
-    pArray = NULL;
-    Aig_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
-    free( pArray );
-
-//    pArray = Abc_NtkGetLatchValues(pNtk2);
-    pArray = NULL;
-    Aig_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
-    free( pArray );
-
-    Aig_ManPrintStats( pMan1 );
-    Aig_ManPrintStats( pMan2 );
-
-    Aig_ManStop( pMan1 );
-    Aig_ManStop( pMan2 );
-
-
-    if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
-    if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -537,7 +488,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 
@@ -573,7 +524,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     Fra_Par_t Pars, * pPars = &Pars; 
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     Fra_ParamsDefault( pPars );
@@ -608,7 +559,7 @@ Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan = Aig_ManFraigPartitioned( pTemp = pMan, nPartSize, nConfLimit, nLevelMax, fVerbose );
@@ -634,7 +585,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
     extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
@@ -661,7 +612,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -705,7 +656,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -742,7 +693,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -774,7 +725,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
@@ -801,7 +752,7 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -910,7 +861,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
     if ( !Aig_ManCheck( pMan ) )
@@ -959,7 +910,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
     assert( Abc_NtkPoNum(pNtk) == 1 );
-    pMan = Abc_NtkToDar( pNtk, 0 );
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
     RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fVerbose ); 
     pNtk->pModel = pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
@@ -993,8 +944,8 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
     // if partitioning is selected, call partitioned CEC
     if ( fPartition )
     {
-        pMan1 = Abc_NtkToDar( pNtk1, 0 );
-        pMan2 = Abc_NtkToDar( pNtk2, 0 );
+        pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
+        pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
         RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, fVerbose );
         Aig_ManStop( pMan1 );
         Aig_ManStop( pMan2 );
@@ -1037,7 +988,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
     }
 
     // derive the AIG manager
-    pMan = Abc_NtkToDar( pMiter, 0 );
+    pMan = Abc_NtkToDar( pMiter, 0, 0 );
     Abc_NtkDelete( pMiter );
     if ( pMan == NULL )
     {
@@ -1106,7 +1057,7 @@ PRT( "Initial fraiging time", clock() - clk );
     else
         pNtkFraig = Abc_NtkDup( pNtk );
 
-    pMan = Abc_NtkToDar( pNtkFraig, 1 );
+    pMan = Abc_NtkToDar( pNtkFraig, 0, 1 );
     Abc_NtkDelete( pNtkFraig );
     if ( pMan == NULL )
         return NULL;
@@ -1143,7 +1094,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
@@ -1178,7 +1129,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, in
     Aig_Man_t * pMan;
     int clk = clock();
     // derive the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
     {
         printf( "Converting miter into AIG has failed.\n" );
@@ -1216,7 +1167,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig
     Aig_Man_t * pMan;
     int RetValue;
     // derive the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
     {
         printf( "Converting miter into AIG has failed.\n" );
@@ -1308,7 +1259,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
     }
 */
     // derive the AIG manager
-    pMan = Abc_NtkToDar( pMiter, 1 );
+    pMan = Abc_NtkToDar( pMiter, 0, 1 );
     Abc_NtkDelete( pMiter );
     if ( pMan == NULL )
     {
@@ -1338,7 +1289,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     Aig_ManSeqCleanup( pMan );
@@ -1366,7 +1317,7 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManReduceLachesCount( pMan );
@@ -1400,7 +1351,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManReduceLachesCount( pMan );
@@ -1434,7 +1385,7 @@ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
 /*
     Aig_Man_t * pMan;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
 //    Aig_ManReduceLachesCount( pMan );
@@ -1463,7 +1414,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
     Fra_Sml_t * pSml;
     Fra_Cex_t * pCex;
     int RetValue, clk = clock();
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
     if ( pSml->fNonConstOut )
     {
@@ -1507,7 +1458,7 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int
         printf( "The number of outputs should be 1.\n" );
         return 1;
     }
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return 1;
 //    Aig_ManReduceLachesCount( pMan );
@@ -1536,7 +1487,7 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
@@ -1573,10 +1524,10 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelat
         return NULL;
     }
     // create internal AIGs
-    pManOn = Abc_NtkToDar( pNtkOn, 0 );
+    pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
     if ( pManOn == NULL )
         return NULL;
-    pManOff = Abc_NtkToDar( pNtkOff, 0 );
+    pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
     if ( pManOff == NULL )
         return NULL;
     // derive the interpolant
@@ -1617,10 +1568,10 @@ void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
     extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
     Aig_Man_t * pManOn, * pManOff;
     // create internal AIGs
-    pManOn = Abc_NtkToDar( pNtkOn, 0 );
+    pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
     if ( pManOn == NULL )
         return;
-    pManOff = Abc_NtkToDar( pNtkOff, 0 );
+    pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
     if ( pManOff == NULL )
         return;
     Aig_ManInterFast( pManOn, pManOff, fVerbose );
@@ -1722,7 +1673,7 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
 {
 //    extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
     Aig_Man_t * pMan;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
     Aig_ManComputeSccs( pMan );
@@ -1730,6 +1681,40 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
     Aig_ManStop( pMan );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Interplates two networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
+{
+    extern void Dar_BalancePrintStats( Aig_Man_t * p );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;//, * pTemp2;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // derive AIG with EXORs
+    pMan = Abc_NtkToDar( pNtk, 1, 0 );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManPrintStats( pMan );
+    if ( fVerbose )
+        Dar_BalancePrintStats( pMan );
+    // perform balancing
+    pTemp = Dar_ManBalance( pMan, fUpdateLevel );
+//    Aig_ManPrintStats( pTemp );
+    // create logic network
+    pNtkAig = Abc_NtkFromDar( pNtk, pTemp );
+    Aig_ManStop( pTemp );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
 
 #include "ntl.h"
 
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 2a2c9d43..fed528ef 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -180,10 +180,21 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 
     assert( Abc_NtkIsLogic(pNtk) );
     nFaninMax = Abc_NtkGetFaninMax(pNtk);
-    if ( nFaninMax > MFS_FANIN_MAX )
+    if ( pPars->fResub )
     {
-        printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX );
-        nFaninMax = MFS_FANIN_MAX;
+        if ( nFaninMax > 8 )
+        {
+            printf( "Nodes with more than %d fanins will node be processed.\n", 8 );
+            nFaninMax = 8;
+        }
+    }
+    else
+    {
+        if ( nFaninMax > MFS_FANIN_MAX )
+        {
+            printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX );
+            nFaninMax = MFS_FANIN_MAX;
+        }
     }
     // perform the network sweep
     Abc_NtkSweep( pNtk, 0 );
@@ -237,41 +248,62 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     nNodes = 0;
     p->nTotalNodesBeg = nTotalNodesBeg;
     p->nTotalEdgesBeg = nTotalEdgesBeg;
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
-    vLevels = Abc_NtkLevelize( pNtk );
-    Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
+    if ( pPars->fResub )
     {
-        if ( !p->pPars->fVeryVerbose )
-            Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
-        p->nNodesGainedLevel = 0;
-        p->nTotConfLevel = 0;
-        p->nTimeOutsLevel = 0;
-        clk2 = clock();
-        Vec_PtrForEachEntry( vNodes, pObj, i )
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+        Abc_NtkForEachNode( pNtk, pObj, i )
         {
             if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
-                break;
-            if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
                 continue;
+            if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
+                continue;
+            if ( !p->pPars->fVeryVerbose )
+                Extra_ProgressBarUpdate( pProgress, i, NULL );
             if ( pPars->fResub )
                 Abc_NtkMfsResub( p, pObj );
-            else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
+            else
                 Abc_NtkMfsNode( p, pObj );
         }
-        nNodes += Vec_PtrSize(vNodes);
-        if ( pPars->fVerbose )
+        Extra_ProgressBarStop( pProgress );
+    }
+    else
+    {
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+        vLevels = Abc_NtkLevelize( pNtk );
+        Vec_VecForEachLevelStart( vLevels, vNodes, k, 1 )
         {
-        printf( "Lev = %2d. Node = %4d. Ave gain = %6.2f. Ave conf = %6.2f. Timeouts = %6.2f %%  ", 
-            k, Vec_PtrSize(vNodes),
-            1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
-            1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
-            100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
-        PRT( "Time", clock() - clk2 );
+            if ( !p->pPars->fVeryVerbose )
+                Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+            p->nNodesGainedLevel = 0;
+            p->nTotConfLevel = 0;
+            p->nTimeOutsLevel = 0;
+            clk2 = clock();
+            Vec_PtrForEachEntry( vNodes, pObj, i )
+            {
+                if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+                    break;
+                if ( Abc_ObjFaninNum(pObj) < 2 || Abc_ObjFaninNum(pObj) > nFaninMax )
+                    continue;
+                if ( pPars->fResub )
+                    Abc_NtkMfsResub( p, pObj );
+                else 
+                    Abc_NtkMfsNode( p, pObj );
+            }
+            nNodes += Vec_PtrSize(vNodes);
+            if ( pPars->fVerbose )
+            {
+            printf( "Lev = %2d. Node = %5d. Ave gain = %5.2f. Ave conf = %5.2f. T/o = %6.2f %%  ", 
+                k, Vec_PtrSize(vNodes),
+                1.0*p->nNodesGainedLevel/Vec_PtrSize(vNodes),
+                1.0*p->nTotConfLevel/Vec_PtrSize(vNodes),
+                100.0*p->nTimeOutsLevel/Vec_PtrSize(vNodes) );
+            PRT( "Time", clock() - clk2 );
+            }
         }
+        Extra_ProgressBarStop( pProgress );
+        Vec_VecFree( vLevels );
     }
-    Extra_ProgressBarStop( pProgress );
     Abc_NtkStopReverseLevels( pNtk );
-    Vec_VecFree( vLevels );
 
     // perform the sweeping
     if ( !pPars->fResub )
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 8908da2f..b6c7299b 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -176,6 +176,7 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
         if ( fVeryVerbose )
         printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
         p->nNodesResub++;
+        p->nNodesGainedLevel++;
         if ( fSkipUpdate )
             return 1;
 clk = clock();
@@ -243,6 +244,7 @@ p->timeInt += clock() - clk;
             if ( fVeryVerbose )
             printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
             p->nNodesResub++;
+            p->nNodesGainedLevel++;
             if ( fSkipUpdate )
                 return 1;
 clk = clock();
@@ -315,6 +317,7 @@ int Abc_NtkMfsSolveSatResub2( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int
         if ( fVeryVerbose )
         printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
         p->nNodesResub++;
+        p->nNodesGainedLevel++;
 clk = clock();
         // derive the function
         pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
@@ -388,6 +391,7 @@ p->timeInt += clock() - clk;
             if ( fVeryVerbose )
             printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
             p->nNodesResub++;
+            p->nNodesGainedLevel++;
 clk = clock();
             // derive the function
             pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );