Version abc60407

52 files changed, 3005 insertions, 289 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c68c74e2..e0f0df99 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -154,6 +154,7 @@ struct Abc_Ntk_t_
     Abc_NtkFunc_t    ntkFunc;       // functionality of the network
     char *           pName;         // the network name
     char *           pSpec;         // the name of the spec file if present
+    int              Id;            // network ID
     // name representation 
     stmm_table *     tName2Net;     // the table hashing net names into net pointer
     stmm_table *     tObj2Name;     // the table hashing PI/PO/latch pointers into names
@@ -210,7 +211,7 @@ struct Abc_Ntk_t_
 // maximum/minimum operators
 #define ABC_MIN(a,b)      (((a) < (b))? (a) : (b))
 #define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
-#define ABC_INFINITY      (10000000)
+#define ABC_INFINITY      (100000000)
 
 // transforming floats into ints and back
 static inline int         Abc_Float2Int( float Val )                 { return *((int *)&Val);               }
@@ -439,10 +440,10 @@ extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose );
+extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
-extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti );
-extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti );
+extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
 extern void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
 extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
 extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
@@ -492,6 +493,8 @@ extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
+extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
+extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
 extern Abc_Ntk_t *        Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
 extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
@@ -554,7 +557,7 @@ extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly, int fReorder, int fVerbose );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
@@ -584,7 +587,7 @@ extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode,
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcProve.c ==========================================================*/
-extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose );
+extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
@@ -607,8 +610,8 @@ extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcSat.c ==========================================================*/
-extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose );
-extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose );
+extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
 extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
@@ -623,6 +626,7 @@ extern char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
+extern char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
 extern int                Abc_SopGetCubeNum( char * pSop );
@@ -672,6 +676,19 @@ extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
 extern int                Abc_NodeReadReverseLevel( Abc_Obj_t * pObj );
 extern int                Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj );
+/*=== abcTrace.c ==========================================================*/
+extern void               Abc_HManStart();
+extern void               Abc_HManStop();
+extern int                Abc_HManIsRunning();
+extern int                Abc_HManGetNewNtkId();
+extern void               Abc_HManAddObj( Abc_Obj_t * pObj );
+extern void               Abc_HManAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern void               Abc_HManXorFaninC( Abc_Obj_t * pObj, int iFanin );
+extern void               Abc_HManRemoveFanins( Abc_Obj_t * pObj );
+extern void               Abc_HManAddProto( Abc_Obj_t * pObj, Abc_Obj_t * pProto );
+extern void               Abc_HManMapAddEqu( Abc_Obj_t * pObj, Abc_Obj_t * pEqu );
+extern int                Abc_HManPopulate( Abc_Ntk_t * pNtk );
+extern int                Abc_HManVerify( int NtkIdOld, int NtkIdNew );
 /*=== abcUtil.c ==========================================================*/
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index f2f50f77..7eb62416 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -807,6 +807,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
         Abc_AigAndDelete( pMan, pFanout );
         // remove the fanins of the old fanout
         Abc_ObjRemoveFanins( pFanout );
+        Abc_HManRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
         assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 59dff196..60e847d0 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -50,6 +50,7 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
+    Abc_HManAddFanin( pObj, pFanin );
 }
 
 
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index cb20cec3..da50a9aa 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_MUX_CUBES   100000
+
 static int         Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
 
 ////////////////////////////////////////////////////////////////////////
@@ -205,6 +207,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
 int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Obj_t * pNode;
+    Extra_MmFlex_t * pManNew;
     DdManager * dd = pNtk->pManFunc;
     DdNode * bFunc;
     Vec_Str_t * vCube;
@@ -217,10 +220,8 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 
     assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
-    // allocate the new manager
-    pNtk->pManFunc = Extra_MmFlexStart();
-    // update the network type
-    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // create the new manager
+    pManNew = Extra_MmFlexStart();
 
     // go through the objects
     vCube = Vec_StrAlloc( 100 );
@@ -228,17 +229,30 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
-        if ( pNode->pData == NULL )
+        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
+        if ( pNode->pNext == NULL )
         {
+            Extra_MmFlexStop( pManNew, 0 );
+            Abc_NtkCleanNext( pNtk );
+//            printf( "Converting from BDDs to SOPs has failed.\n" );
             Vec_StrFree( vCube );
-            Cudd_Quit( dd );
             return 0;
         }
-        Cudd_RecursiveDeref( dd, bFunc );
     }
     Vec_StrFree( vCube );
 
+    // update the network type
+    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // set the new manager
+    pNtk->pManFunc = pManNew;
+    // transfer from next to data
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = pNode->pNext;
+        pNode->pNext = NULL;
+    }
+
     // check for remaining references in the package
     Extra_StopManager( dd );
     return 1;
@@ -339,6 +353,13 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
         assert( 0 );
     }
 
+    if ( nCubes > ABC_MUX_CUBES )
+    {
+        Cudd_RecursiveDerefZdd( dd, zCover );
+        printf( "The number of cubes exceeded the predefined limit (%d).\n", ABC_MUX_CUBES );
+        return NULL;
+    }
+
     // allocate memory for the cover
     if ( pMan )
         pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
@@ -468,6 +489,8 @@ void Abc_CountZddCubes_rec( DdManager * dd, DdNode * zCover, int * pnCubes )
         (*pnCubes)++;
         return;
     }
+    if ( (*pnCubes) > ABC_MUX_CUBES )
+        return;
     extraDecomposeCover( dd, zCover, &zC0, &zC1, &zC2 );
     Abc_CountZddCubes_rec( dd, zC0, pnCubes );
     Abc_CountZddCubes_rec( dd, zC1, pnCubes );
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index d289cd35..737d63c2 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -62,7 +62,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pFanin)->pCopy );
     // collect the CO nodes
     Abc_NtkFinalize( pNtk, pNtkNew );
-    // fix the problem with CO pointing directing to CIs
+    // fix the problem with CO pointing directly to CIs
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate EXDC 
     if ( pNtk->pExdc )
@@ -101,7 +101,8 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
     }
     else if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        Abc_NtkBddToSop(pNtk, fDirect);
+        if ( !Abc_NtkBddToSop(pNtk, fDirect) )
+            return NULL;
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
         Abc_NtkSopToBdd(pNtk);
     }
@@ -157,7 +158,10 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk,0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk,0) )
+            return NULL;
+    }
 
     // start the netlist by creating PI/PO/Latch objects
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc );
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 0692819b..60ad2412 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -50,6 +50,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     memset( pNtk, 0, sizeof(Abc_Ntk_t) );
     pNtk->ntkType     = Type;
     pNtk->ntkFunc     = Func;
+    pNtk->Id          = !Abc_HManIsRunning()? 0 : Abc_HManGetNewNtkId();
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
     pNtk->vLats       = Vec_PtrAlloc( 100 );
@@ -136,6 +137,14 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Vec_PtrPush( pNtkNew->vCis, pObjNew );
         Vec_PtrPush( pNtkNew->vCos, pObjNew );
     }
+    if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
+    {
+        Abc_HManAddProto( Abc_NtkConst1(pNtk)->pCopy, Abc_NtkConst1(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+    }
     // transfer the names
     Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
     Abc_ManTimeDup( pNtk, pNtkNew );
@@ -407,6 +416,11 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     }
+    if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_HManAddProto( pObj->pCopy, pObj );
+    }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index d6adfeb2..0ffe3298 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -50,6 +50,8 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
     pObj->pNtk = pNtk;
     pObj->Type = Type;
     pObj->Id   = -1;
+    if ( pNtk->ntkType != ABC_NTK_NETLIST )
+        Abc_HManAddObj( pObj );
     return pObj;
 }
 
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 1e59b17b..d5cc65f1 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -61,7 +61,7 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+  Synopsis    [Creates the constant 1 cover with the given number of variables and cubes.]
 
   Description []
                
@@ -92,7 +92,7 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with 0 variables.]
+  Synopsis    [Creates the constant 1 cover with 0 variables.]
 
   Description []
                
@@ -108,7 +108,7 @@ char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the constant 1 cover with 0 variables.]
+  Synopsis    [Creates the constant 1 cover with 0 variables.]
 
   Description []
                
@@ -124,7 +124,7 @@ char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the AND2 cover.]
+  Synopsis    [Creates the AND2 cover.]
 
   Description []
                
@@ -147,7 +147,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input AND cover.]
+  Synopsis    [Creates the multi-input AND cover.]
 
   Description []
                
@@ -169,7 +169,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input NAND cover.]
+  Synopsis    [Creates the multi-input NAND cover.]
 
   Description []
                
@@ -191,7 +191,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input OR cover.]
+  Synopsis    [Creates the multi-input OR cover.]
 
   Description []
                
@@ -213,7 +213,7 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input OR cover.]
+  Synopsis    [Creates the multi-input OR cover.]
 
   Description []
                
@@ -238,7 +238,7 @@ char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input NOR cover.]
+  Synopsis    [Creates the multi-input NOR cover.]
 
   Description []
                
@@ -259,7 +259,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XOR cover.]
+  Synopsis    [Creates the multi-input XOR cover.]
 
   Description []
                
@@ -276,7 +276,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XOR cover (special case).]
+  Synopsis    [Creates the multi-input XOR cover (special case).]
 
   Description []
                
@@ -296,7 +296,7 @@ char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the multi-input XNOR cover.]
+  Synopsis    [Creates the multi-input XNOR cover.]
 
   Description []
                
@@ -313,7 +313,24 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the inv cover.]
+  Synopsis    [Creates the MUX cover.]
+
+  Description [The first input of MUX is the control. The second input
+  is DATA1. The third input is DATA0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateMux( Extra_MmFlex_t * pMan )
+{
+    return Abc_SopRegister(pMan, "11- 1\n0-1 1\n");
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the inv cover.]
 
   Description []
                
@@ -329,7 +346,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the buf cover.]
+  Synopsis    [Creates the buf cover.]
 
   Description []
                
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ffab5116..26ef2b66 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -64,6 +64,7 @@ static int Abc_CommandRewrite      ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandRefactor     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRestructure  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRr           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -82,6 +83,7 @@ static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEspresso     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGen          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -115,6 +117,9 @@ static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandTraceStart   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTraceCheck   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -167,6 +172,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "restructure",   Abc_CommandRestructure,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "rr",            Abc_CommandRr,               1 );
 
 //    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
@@ -185,6 +191,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
+    Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -218,9 +225,13 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
 
+    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
+    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
+
 //    Rwt_Man4ExploreStart();
 //    Map_Var3Print();
 //    Map_Var4Test();
+
 }
 
 /**Function*************************************************************
@@ -1598,6 +1609,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int fBddSizeMax;
     int fDualRail;
+    int fReorder;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -1605,10 +1617,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fReorder = 1;
     fDualRail = 0;
     fBddSizeMax = 1000000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Bdh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Brdh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1626,6 +1639,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDualRail ^= 1;
             break;
+        case 'r':
+            fReorder ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -1647,11 +1663,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0 );
-        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -1664,9 +1680,10 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: collapse [-B num] [-dh]\n" );
+    fprintf( pErr, "usage: collapse [-B num] [-rdh]\n" );
     fprintf( pErr, "\t          collapses the network by constructing global BDDs\n" );
     fprintf( pErr, "\t-B num  : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
+    fprintf( pErr, "\t-r      : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" );
     fprintf( pErr, "\t-d      : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
@@ -2759,6 +2776,102 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c, Window;
+    int nFaninLevels;
+    int nFanoutLevels;
+    int fUseFanouts;
+    int fVerbose;
+    extern int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFaninLevels  = 3;
+    nFanoutLevels = 3;
+    fUseFanouts   = 0;
+    fVerbose      = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Wfvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Window = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Window < 0 ) 
+                goto usage;
+            nFaninLevels  = Window / 10;
+            nFanoutLevels = Window % 10;
+            break;
+        case 'f':
+            fUseFanouts ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" );
+        return 1;
+    }
+    if ( Abc_NtkGetChoiceNum(pNtk) )
+    {
+        fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
+        return 1;
+    }
+
+    // modify the current network
+    if ( !Abc_NtkRR( pNtk, nFaninLevels, nFanoutLevels, fUseFanouts, fVerbose ) )
+    {
+        fprintf( pErr, "Redundancy removal has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rr [-W NM] [-fvh]\n" );
+    fprintf( pErr, "\t         performs redundancy removal in the current network\n" );
+    fprintf( pErr, "\t-W NM  : window size as the number of TFI (N) and TFO (M) logic levels [default = %d%d]\n", nFaninLevels, nFanoutLevels );
+    fprintf( pErr, "\t-f     : toggle RR w.r.t. fanouts [default = %s]\n", fUseFanouts? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -3806,10 +3919,12 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fTruth    = 0;     // compute truth tables
     pParams->fFilter   = 1;     // filter dominated cuts
     pParams->fDrop     = 0;     // drop cuts on the fly
-    pParams->fMulti    = 0;     // use multi-input AND-gates
+    pParams->fDag      = 0;     // compute DAG cuts
+    pParams->fTree     = 0;     // compute tree cuts
+    pParams->fFancy    = 0;     // compute something fancy
     pParams->fVerbose  = 0;     // the verbosiness flag
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdmvoh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyzvoh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3844,8 +3959,14 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pParams->fDrop ^= 1;
             break;
-        case 'm':
-            pParams->fMulti ^= 1;
+        case 'x':
+            pParams->fDag ^= 1;
+            break;
+        case 'y':
+            pParams->fTree ^= 1;
+            break;
+        case 'z':
+            pParams->fFancy ^= 1;
             break;
         case 'v':
             pParams->fVerbose ^= 1;
@@ -3875,6 +3996,11 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", CUT_SIZE_MIN, CUT_SIZE_MAX );
         return 1;
     }
+    if ( pParams->fDag && pParams->fTree )
+    {
+        fprintf( pErr, "Cannot compute both DAG cuts and tree cuts at the same time.\n" );
+        return 1;
+    }
 
     if ( fOracle )
         pParams->fRecord = 1;
@@ -3891,14 +4017,16 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdmvh]\n" );
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzvh]\n" );
     fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
     fprintf( pErr, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n",   CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax );
     fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",      pParams->nKeepMax );
     fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",           pParams->fTruth?   "yes": "no" );
     fprintf( pErr, "\t-f     : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter?  "yes": "no" );
     fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop?    "yes": "no" );
-    fprintf( pErr, "\t-m     : toggle computing only factor-cuts [default = %s]\n",        pParams->fMulti?   "yes": "no" );
+    fprintf( pErr, "\t-x     : toggle computing only DAG cuts [default = %s]\n",           pParams->fDag?     "yes": "no" );
+    fprintf( pErr, "\t-y     : toggle computing only tree cuts [default = %s]\n",          pParams->fTree?    "yes": "no" );
+    fprintf( pErr, "\t-z     : toggle fancy computations [default = %s]\n",                pParams->fFancy?   "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -4160,6 +4288,99 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nVars;
+    int fAdder;
+    int fSorter;
+    int fVerbose;
+    char * FileName;
+    extern void Abc_GenAdder( char * pFileName, int nVars );
+    extern void Abc_GenSorter( char * pFileName, int nVars );
+
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nVars = 8;
+    fAdder = 0;
+    fSorter = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVars < 0 ) 
+                goto usage;
+            break;
+        case 'a':
+            fAdder ^= 1;
+            break;
+        case 's':
+            fSorter ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( fAdder )
+        Abc_GenAdder( FileName, nVars );
+    else if ( fSorter )
+        Abc_GenSorter( FileName, nVars );
+    else
+        printf( "Type of circuit is not specified.\n" );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: gen [-N] [-asvh] <file>\n" );
+    fprintf( pErr, "\t         generates simple circuits\n" );
+    fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars );  
+    fprintf( pErr, "\t-a     : toggle ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
+    fprintf( pErr, "\t-s     : toggle simple sorter [default = %s]\n", fSorter? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : output file name\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -4175,7 +4396,7 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
     int c;
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 
@@ -4195,25 +4416,27 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+/*
     if ( pNtk == NULL )
     {
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-
     if ( Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Only works for non-sequential networks.\n" );
         return 1;
     }
+*/
 
 //    Abc_NtkTestEsop( pNtk );
 //    Abc_NtkTestSop( pNtk );
 //    printf( "This command is currently not used.\n" );
     // run the command
 //    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
-
 //    pNtkRes = Abc_NtkNewAig( pNtk );
+
+/*
     pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
@@ -4222,6 +4445,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
+
+//    if ( Cut_CellIsRunning() )
+//        Cut_CellDumpToFile();
+//    else
+//        Cut_CellPrecompute();
+        Cut_CellLoad();
+
     return 0;
 
 usage:
@@ -6459,6 +6690,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int RetValue;
+    int fJFront;
     int fVerbose;
     int nConfLimit;
     int nImpLimit;
@@ -6469,11 +6701,12 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fJFront = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nImpLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvjh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6499,6 +6732,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nImpLimit < 0 ) 
                 goto usage;
             break;
+        case 'j':
+            fJFront ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6528,13 +6764,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     clk = clock();
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fJFront, fVerbose );
     }
     else
     {
         Abc_Ntk_t * pTemp;
         pTemp = Abc_NtkStrash( pNtk, 0, 0 );
-        RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose );
+        RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fJFront, fVerbose );
         pNtk->pModel = pTemp->pModel;  pTemp->pModel = NULL;
         Abc_NtkDelete( pTemp );
     }
@@ -6544,7 +6780,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
         if ( pSimInfo[0] != 1 )
-            printf( "ERROR in Abc_NtkMiterProve(): Generated counter example is invalid.\n" );
+            printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
         free( pSimInfo );
     }
 
@@ -6559,11 +6795,12 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
+    fprintf( pErr, "usage: sat [-C num] [-I num] [-jvh]\n" );
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
+    fprintf( pErr, "\t-j     : toggle the use of J-frontier [default = %s]\n", fJFront? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -6584,60 +6821,72 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int c;
-    int RetValue;
-    int fVerbose; 
-    int fRewrite;
-    int fFraig;
-    int nConfLimit;
-    int nImpLimit;
-    int clk;
+    Prove_Params_t Params, * pParams = &Params;
+    int c, clk, RetValue;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose   = 0;
-    fRewrite   = 1;
-    fFraig     = 1;
-    nConfLimit = 300000;   
-    nImpLimit  = 0;
+    Prove_ParamsSetDefault( pParams );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIrfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NCFLrfvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nItersMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pParams->nItersMax < 0 ) 
+                goto usage;
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
                 fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nConfLimit = atoi(argv[globalUtilOptind]);
+            pParams->nMiteringLimitStart = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nConfLimit < 0 ) 
+            if ( pParams->nMiteringLimitStart < 0 ) 
                 goto usage;
             break;
-        case 'I':
+        case 'F':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nImpLimit = atoi(argv[globalUtilOptind]);
+            pParams->nFraigingLimitStart = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nImpLimit < 0 ) 
+            if ( pParams->nFraigingLimitStart < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nMiteringLimitLast = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pParams->nMiteringLimitLast < 0 ) 
                 goto usage;
             break;
         case 'r':
-            fRewrite ^= 1;
+            pParams->fUseRewriting ^= 1;
             break;
         case 'f':
-            fFraig ^= 1;
+            pParams->fUseFraiging ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pParams->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -6674,7 +6923,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
         pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
 
-    RetValue = Abc_NtkMiterProve( &pNtkTemp, nConfLimit, nImpLimit, fRewrite, fFraig, fVerbose );
+    RetValue = Abc_NtkMiterProve( &pNtkTemp, pParams );
 
     // verify that the pattern is correct
     if ( RetValue == 0 )
@@ -6699,19 +6948,143 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: prove [-C num] [-I num] [-rfvh]\n" );
+    fprintf( pErr, "usage: prove [-N num] [-C num] [-F num] [-L num] [-rfvh]\n" );
     fprintf( pErr, "\t         solves combinational miter by rewriting, FRAIGing, and SAT\n" );
     fprintf( pErr, "\t         replaces the current network by the cone modified by rewriting\n" );
-    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-    fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
-    fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );  
-    fprintf( pErr, "\t-f     : toggle the use of FRAIGing [default = %s]\n", fFraig? "yes": "no" );  
-    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-N num : max number of iterations [default = %d]\n", pParams->nItersMax );
+    fprintf( pErr, "\t-C num : max starting number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitStart );
+    fprintf( pErr, "\t-F num : max starting number of conflicts in fraiging [default = %d]\n", pParams->nFraigingLimitStart );
+    fprintf( pErr, "\t-L num : max last-gasp number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitLast );
+    fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" );  
+    fprintf( pErr, "\t-f     : toggle the use of FRAIGing [default = %s]\n", pParams->fUseFraiging? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command is applicable to AIGs.\n" );
+        return 1;
+    }
+
+    Abc_HManStart();
+    if ( !Abc_HManPopulate( pNtk ) )
+    {
+        fprintf( pErr, "Failed to start the tracing database.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: trace_start [-h]\n" );
+    fprintf( pErr, "\t        starts verification tracing\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTraceCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command is applicable to AIGs.\n" );
+        return 1;
+    }
+
+    if ( !Abc_HManIsRunning(pNtk) )
+    {
+        fprintf( pErr, "The tracing database is not available.\n" );
+        return 1;
+    }
+
+    if ( !Abc_HManVerify( 1, pNtk->Id ) )
+        fprintf( pErr, "Verification failed.\n" );
+    Abc_HManStop();
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: trace_check [-h]\n" );
+    fprintf( pErr, "\t        checks the current network using verification trace\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index fb818ff3..cc6e8913 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -51,7 +51,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
     int nOutputs, nInputs, i;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
         return;
 
     // get information about the network
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 919ea3b2..9e9212aa 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -29,6 +29,8 @@ static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode,
 static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective );
 static int         Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective );
 static void        Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk );
+static Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -227,6 +229,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
         return pNodeOld->pCopy;
     assert( Abc_ObjIsNode(pNodeOld) );
     // get the implication supergate
+//    Abc_NodeBalanceConeExor( pNodeOld );
     vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective );
     if ( vSuper->nSize == 0 )
     { // it means that the supergate contains two nodes in the opposite polarity
@@ -260,6 +263,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     assert( pNodeOld->pCopy == NULL );
     // mark the old node with the new node
     pNodeOld->pCopy = vSuper->pArray[0];
+    Abc_HManAddProto( pNodeOld->pCopy, pNodeOld );
     vSuper->nSize = 0;
     return pNodeOld->pCopy;
 }
@@ -351,6 +355,65 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeBalanceConeExor_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst )
+{
+    int RetValue1, RetValue2, i;
+    // check if the node occurs in the same polarity
+    for ( i = 0; i < vSuper->nSize; i++ )
+        if ( vSuper->pArray[i] == pNode )
+            return 1;
+    // if the new node is complemented or a PI, another gate begins
+    if ( !fFirst && (!pNode->fExor || !Abc_ObjIsNode(pNode)) )
+    {
+        Vec_PtrPush( vSuper, pNode );
+        return 0;
+    }
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    assert( pNode->fExor );
+    // go through the branches
+    RetValue1 = Abc_NodeBalanceConeExor_rec( Abc_ObjFanin0(Abc_ObjFanin0(pNode)), vSuper, 0 );
+    RetValue2 = Abc_NodeBalanceConeExor_rec( Abc_ObjFanin1(Abc_ObjFanin0(pNode)), vSuper, 0 );
+    if ( RetValue1 == -1 || RetValue2 == -1 )
+        return -1;
+    // return 1 if at least one branch has a duplicate
+    return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vSuper;
+    if ( !pNode->fExor )
+        return NULL;
+    vSuper = Vec_PtrAlloc( 10 );
+    Abc_NodeBalanceConeExor_rec( pNode, vSuper, 1 );
+    printf( "%d ", Vec_PtrSize(vSuper) );
+    Vec_PtrFree( vSuper );
+    return NULL;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index 84016436..eed18e1b 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -43,14 +43,14 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 2b1816c4..2752dc69 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -29,6 +29,9 @@
 static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
 static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
 
+
+extern int nTotal, nGood, nEqual;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,6 +49,7 @@ static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
 ***********************************************************************/
 Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
+    ProgressBar * pProgress;
     Cut_Man_t *  p;
     Abc_Obj_t * pObj, * pNode;
     Vec_Ptr_t * vNodes;
@@ -56,6 +60,8 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
     extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
 
+    nTotal = nGood = nEqual = 0;
+
     assert( Abc_NtkIsStrash(pNtk) );
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
@@ -69,6 +75,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     // compute cuts for internal nodes
     vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
     vChoices = Vec_IntAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // when we reached a CO, it is time to deallocate the cuts
@@ -81,8 +88,9 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
         // skip constant node, it has no cuts
         if ( Abc_NodeIsConst(pObj) )
             continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
         // compute the cuts to the internal node
-        Abc_NodeGetCuts( p, pObj, pParams->fMulti );  
+        Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree );  
         // consider dropping the fanins cuts
         if ( pParams->fDrop )
         {
@@ -98,11 +106,16 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
             Cut_NodeUnionCuts( p, vChoices );
         }
     }
+    Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
 PRT( "Total", clock() - clk );
 //Abc_NtkPrintCuts_( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
+
+    // temporary printout of stats
+    if ( nTotal )
+    printf( "Total cuts = %d. Good cuts = %d.  Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal );
     return p;
 }
 
@@ -276,14 +289,14 @@ printf( "Converged after %d iterations.\n", nIters );
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti )
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
     void * pList;
     if ( pList = Abc_NodeReadCuts( p, pObj ) )
         return pList;
-    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fMulti );
-    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fMulti );
-    return Abc_NodeGetCuts( p, pObj, fMulti );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree );
+    return Abc_NodeGetCuts( p, pObj, fDag, fTree );
 }
 
 /**Function*************************************************************
@@ -297,14 +310,28 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti )
+void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
-//    int fTriv = (!fMulti) || pObj->fMarkB;
-    int fTriv = (!fMulti) || (pObj->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pObj));
+    Abc_Obj_t * pFanin;
+    int fDagNode, fTriv, TreeCode = 0;
     assert( Abc_NtkIsStrash(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
+    // check if the node is a DAG node
+    fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
+    // increment the counter of DAG nodes
+    if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+    // add the trivial cut if the node is a DAG node, or if we compute all cuts
+    fTriv = fDagNode || !fDag;
+    // check if fanins are DAG nodes
+    if ( fTree )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        TreeCode |=  (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin));
+        pFanin = Abc_ObjFanin1(pObj);
+        TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1);
+    }
     return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
-        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv );  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode );  
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 18a85a04..79d2b729 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
index 744169b5..ad43534d 100644
--- a/src/base/abci/abcEspresso.c
+++ b/src/base/abci/abcEspresso.c
@@ -54,7 +54,13 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
     if ( Abc_NtkHasMapping(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
     // minimize SOPs of all nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( i ) Abc_NodeEspresso( pNode );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 4aae6ba5..2f54dcee 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -684,7 +684,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
         // set the number of networks stored
         Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
     }
-    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
     return 1;
 }
 
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index b377da1d..a8e656ce 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -57,7 +57,13 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     if ( Abc_NtkIsMappedLogic(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return 0;
+        }
+    }
     else
     { // to make sure the SOPs are SCC-free
 //        Abc_NtkSopToBdd(pNtk);
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
new file mode 100644
index 00000000..626e5e1e
--- /dev/null
+++ b/src/base/abci/abcGen.c
@@ -0,0 +1,261 @@
+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+void Abc_WriteLayer( FILE * pFile, int nVars, int fSkip1 );
+void Abc_WriteComp( FILE * pFile );
+void Abc_WriteFullAdder( FILE * pFile );
+
+void Abc_GenAdder( char * pFileName, int nVars );
+void Abc_GenSorter( char * pFileName, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenAdder( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i;
+
+    assert( nVars > 0 );
+
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# %d-bit ripple-carry adder generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model Adder%02d\n", nVars );
+
+    fprintf( pFile, ".inputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " a%02d", i );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " b%02d", i );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".outputs" );
+    for ( i = 0; i <= nVars; i++ )
+        fprintf( pFile, " y%02d", i );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".names c\n" );
+    if ( nVars == 1 )
+        fprintf( pFile, ".subckt FA a=a00 b=b00 cin=c s=y00 cout=y01\n" );
+    else
+    {
+        fprintf( pFile, ".subckt FA a=a00 b=b00 cin=c s=y00 cout=%02d\n", 0 );
+        for ( i = 1; i < nVars-1; i++ )
+            fprintf( pFile, ".subckt FA a=a%02d b=b%02d cin=%02d s=y%02d cout=%02d\n", i, i, i-1, i, i );
+        fprintf( pFile, ".subckt FA a=a%02d b=b%02d cin=%02d s=y%02d cout=y%02d\n", i, i, i-1, i, i+1 );
+    }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" );
+
+    Abc_WriteFullAdder( pFile );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenSorter( char * pFileName, int nVars )
+{
+    FILE * pFile;
+    int i, k, Counter, nDigits;
+
+    assert( nVars > 1 );
+
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# %d-bit sorter generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model Sorter%02d\n", nVars );
+
+    fprintf( pFile, ".inputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " x%02d", i );
+    fprintf( pFile, "\n" );
+
+    fprintf( pFile, ".outputs" );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " y%02d", i );
+    fprintf( pFile, "\n" );
+
+    Counter = 0;
+    nDigits = Extra_Base10Log( (nVars-2)*nVars );
+    if ( nVars == 2 )
+        fprintf( pFile, ".subckt Comp a=x00 b=x01 x=y00 y=y01\n" );
+    else
+    {
+        fprintf( pFile, ".subckt Layer0" );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " x%02d=x%02d", k, k );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
+        fprintf( pFile, "\n" );
+        Counter -= nVars;
+        for ( i = 1; i < nVars-2; i++ )
+        {
+            fprintf( pFile, ".subckt Layer%d", (i&1) );
+            for ( k = 0; k < nVars; k++ )
+                fprintf( pFile, " x%02d=%0*d", k, nDigits, Counter++ );
+            for ( k = 0; k < nVars; k++ )
+                fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
+            fprintf( pFile, "\n" );
+            Counter -= nVars;
+        }
+        fprintf( pFile, ".subckt Layer%d", (i&1) );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " x%02d=%0*d", k, nDigits, Counter++ );
+        for ( k = 0; k < nVars; k++ )
+            fprintf( pFile, " y%02d=y%02d", k, k );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" );
+
+    Abc_WriteLayer( pFile, nVars, 0 );
+    Abc_WriteLayer( pFile, nVars, 1 );
+    Abc_WriteComp( pFile );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteLayer( FILE * pFile, int nVars, int fSkip1 )
+{
+    int i;
+    fprintf( pFile, ".model Layer%d\n", fSkip1 );
+    fprintf( pFile, ".inputs" ); 
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " x%02d", i ); 
+    fprintf( pFile, "\n" ); 
+    fprintf( pFile, ".outputs" ); 
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " y%02d", i ); 
+    fprintf( pFile, "\n" ); 
+    if ( fSkip1 )
+    {
+        fprintf( pFile, ".names x00 y00\n" ); 
+        fprintf( pFile, "1 1\n" ); 
+        i = 1;
+    }
+    else
+        i = 0;
+    for ( ; i + 1 < nVars; i += 2 )
+        fprintf( pFile, ".subckt Comp a=x%02d b=x%02d x=y%02d y=y%02d\n", i, i+1, i, i+1 );
+    if ( i < nVars )
+    {
+        fprintf( pFile, ".names x%02d y%02d\n", i, i ); 
+        fprintf( pFile, "1 1\n" ); 
+    }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteComp( FILE * pFile )
+{
+    fprintf( pFile, ".model Comp\n" );
+    fprintf( pFile, ".inputs a b\n" ); 
+    fprintf( pFile, ".outputs x y\n" ); 
+    fprintf( pFile, ".names a b x\n" ); 
+    fprintf( pFile, "11 1\n" ); 
+    fprintf( pFile, ".names a b y\n" ); 
+    fprintf( pFile, "1- 1\n" ); 
+    fprintf( pFile, "-1 1\n" ); 
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_WriteFullAdder( FILE * pFile )
+{
+    fprintf( pFile, ".model FA\n" );
+    fprintf( pFile, ".inputs a b cin\n" ); 
+    fprintf( pFile, ".outputs s cout\n" ); 
+    fprintf( pFile, ".names a b k\n" ); 
+    fprintf( pFile, "10 1\n" ); 
+    fprintf( pFile, "01 1\n" ); 
+    fprintf( pFile, ".names k cin s\n" ); 
+    fprintf( pFile, "10 1\n" ); 
+    fprintf( pFile, "01 1\n" ); 
+    fprintf( pFile, ".names a b cin cout\n" ); 
+    fprintf( pFile, "11- 1\n" ); 
+    fprintf( pFile, "1-1 1\n" ); 
+    fprintf( pFile, "-11 1\n" ); 
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 25d9e30f..c579eb84 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -522,7 +522,11 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
     pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 );
-    Abc_NtkBddToSop( pNtkNew, 0 );
+    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+    {
+        printf( "Converting to SOPs has failed.\n" );
+        return NULL;
+    }
 
     // set the old network to point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index c0658d5e..87ea57f3 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -282,7 +282,129 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the AND of two miters.]
+
+  Description [The network should have the same names of PIs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    char Buffer[100];
+    Abc_Ntk_t * pNtkMiter;
+    Abc_Obj_t * pOutput1, * pOutput2;
+    Abc_Obj_t * pRoot1, * pRoot2, * pMiter;
+
+    assert( Abc_NtkIsStrash(pNtk1) );
+    assert( Abc_NtkIsStrash(pNtk2) );
+    assert( 1 == Abc_NtkCoNum(pNtk1) );
+    assert( 1 == Abc_NtkCoNum(pNtk2) );
+    assert( 0 == Abc_NtkLatchNum(pNtk1) );
+    assert( 0 == Abc_NtkLatchNum(pNtk2) );
+    assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
+
+    // start the new network
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
+    pNtkMiter->pName = Extra_UtilStrsav(Buffer);
+
+    // perform strashing
+    Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1 );
+    Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
+    Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
+//    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, 1 );
+    pRoot1 = Abc_NtkPo(pNtk1,0);
+    pRoot2 = Abc_NtkPo(pNtk2,0);
+    pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) );
+    pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) );
+
+    // create the miter of the two outputs
+    pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 );
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkMiter ) )
+    {
+        printf( "Abc_NtkMiterAnd: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkMiter );
+        return NULL;
+    }
+    return pNtkMiter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cofactor of the miter w.r.t. the set of vars.]
+
+  Description [The array of variable values contains -1/0/1 for each PI.
+  -1 means this PI remains, 0/1 means this PI is set to 0/1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
+{
+    char Buffer[100];
+    Abc_Ntk_t * pNtkMiter;
+    Abc_Obj_t * pRoot, * pOutput1;
+    int Value, i;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( 1 == Abc_NtkCoNum(pNtk) );
+
+    // start the new network
+    pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    sprintf( Buffer, "%s_miter", pNtk->pName );
+    pNtkMiter->pName = Extra_UtilStrsav(Buffer);
+
+    // get the root output
+    pRoot = Abc_NtkCo( pNtk, 0 );
+
+    // perform strashing
+    Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
+    // set the first cofactor
+    Vec_IntForEachEntry( vPiValues, Value, i )
+    {
+        if ( Value == -1 )
+            continue;
+        if ( Value == 0 )
+        {
+            Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) );
+            continue;
+        }
+        if ( Value == 1 )
+        {
+            Abc_NtkCi(pNtk, i)->pCopy = Abc_NtkConst1(pNtkMiter);
+            continue;
+        }
+        assert( 0 );
+    }
+    // add the first cofactor
+    Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
+
+    // save the output
+    pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
+
+    // create the miter of the two outputs
+    Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pOutput1 );
 
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkMiter ) )
+    {
+        printf( "Abc_NtkMiterCofactor: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkMiter );
+        return NULL;
+    }
+    return pNtkMiter;
+}
 /**Function*************************************************************
 
   Synopsis    [Derives the miter of two cofactors of one output.]
diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c
index 209fc991..62ae51ed 100644
--- a/src/base/abci/abcNewAig.c
+++ b/src/base/abci/abcNewAig.c
@@ -65,7 +65,13 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index d92da31b..33f432f4 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -27,7 +27,7 @@
 static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
-static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -243,15 +243,14 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly )
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly, int fReorder, int fVerbose )
 {
-    int fReorder = 1;
     ProgressBar * pProgress;
     Vec_Ptr_t * vFuncsGlob;
     Abc_Obj_t * pNode;
     DdNode * bFunc;
     DdManager * dd;
-    int i;
+    int i, Counter;
 
     // start the manager
     assert( pNtk->pManGlob == NULL );
@@ -269,18 +268,20 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
 
     // collect the global functions of the COs
     vFuncsGlob = Vec_PtrAlloc( 100 );
+    Counter = 0;
     if ( fLatchOnly )
     {
         // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) );
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachLatch( pNtk, pNode, i )
         {
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
+//            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
+                if ( fVerbose )
                 printf( "Constructing global BDDs is aborted.\n" );
-                Extra_ProgressBarStop( pProgress );
+                Vec_PtrFree( vFuncsGlob );
                 Cudd_Quit( dd );
                 return NULL;
             }
@@ -292,15 +293,16 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
     else
     {
         // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
+//            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose );
             if ( bFunc == NULL )
             {
+                if ( fVerbose )
                 printf( "Constructing global BDDs is aborted.\n" );
-                Extra_ProgressBarStop( pProgress );
+                Vec_PtrFree( vFuncsGlob );
                 Cudd_Quit( dd );
                 return NULL;
             }
@@ -339,12 +341,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax )
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
 {
     DdNode * bFunc, * bFunc0, * bFunc1;
     assert( !Abc_ObjIsComplement(pNode) );
     if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
     {
+        Extra_ProgressBarStop( pProgress );
+        if ( fVerbose )
         printf( "The number of live nodes reached %d.\n", nBddSizeMax );
         fflush( stdout );
         return NULL;
@@ -353,11 +357,11 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
     if ( pNode->pCopy )
         return (DdNode *)pNode->pCopy;
     // compute the result for both branches
-    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax ); 
+    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
     if ( bFunc0 == NULL )
         return NULL;
     Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax ); 
+    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
     if ( bFunc1 == NULL )
         return NULL;
     Cudd_Ref( bFunc1 );
@@ -370,6 +374,9 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
     // set the result
     assert( pNode->pCopy == NULL );
     pNode->pCopy = (Abc_Obj_t *)bFunc;
+    // increment the progress bar
+    if ( pProgress )
+        Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL );
     return bFunc;
 }
 
@@ -427,7 +434,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
     // build the BDD of the cone
-    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000 );  Cudd_Ref( bFunc );
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, NULL, NULL, 1 );  Cudd_Ref( bFunc );
     bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
     // count minterms
     Result = Cudd_CountMinterm( dd, bFunc, dd->size );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index d299a29d..56b70c5b 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -28,6 +28,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+//extern int s_TotalNodes = 0;
+//extern int s_TotalChanges = 0;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -147,6 +150,11 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fclose( pTable );
     }
 */
+/*
+    s_TotalNodes += Abc_NtkNodeNum(pNtk);
+    printf( "Total nodes = %6d   %6.2f Mb   Changes = %6d.\n", 
+        s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges );
+*/
 }
 
 /**Function*************************************************************
@@ -644,7 +652,13 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
 
     // get hold of the SOP of the node
     CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0;
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index ae4bb250..c0e904bf 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "fraig.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -32,10 +33,11 @@ extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
- 
+  
 /**Function*************************************************************
 
   Synopsis    [Attempts to solve the miter using a number of tricks.]
@@ -50,106 +52,126 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
+int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
+    Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;  // was 5000
-    int nConfs, nImps, nBTLimit, RetValue, nSatFails;
-    int nIter = 0, clk, timeStart = clock();
+    int RetValue, nIter, Counter, clk, timeStart = clock();
 
     // get the starting network
     pNtk = *ppNtk;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
 
-    // set the initial limits
-    nConfs   = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit );
-    nImps    = !nImpLimit ? nImpsStart  : ABC_MIN( nImpsStart , nImpLimit );
-    nBTLimit = nBTLimitStart;
-
-    if ( fVerbose )
-        printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit );
+    if ( pParams->fVerbose )
+    {
+        printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
+            pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
+        printf( "Mitering = %d (%3.1f).  Rewriting = %d (%3.1f).  Fraiging = %d (%3.1f).\n", 
+            pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
+            pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
+            pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti );
+        printf( "Mitering last = %d.\n", 
+            pParams->nMiteringLimitLast );
+    }
 
     // if SAT only, solve without iteration
-    if ( !fUseRewrite && !fUseFraig )
+    if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
-        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         *ppNtk = pNtk;
         return RetValue;
     }
 
     // check the current resource limits
-    do {
-        nIter++;
-
-        if ( fVerbose )
+    for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
+    {
+        if ( pParams->fVerbose )
         {
-            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
+                 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
+                 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
             fflush( stdout );
         }
 
         // try brute-force SAT
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 );
-        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 0, 0, 0 );
+        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         if ( RetValue >= 0 )
             break;
 
-        if ( fUseRewrite )
+        // try rewriting
+        if ( pParams->fUseRewriting )
         {
             clk = clock();
-
-            // try rewriting
-            Abc_NtkRewrite( pNtk, 0, 0, 0 );
-            if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
-                break;
-            Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
-            if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
-                break;
-            pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
-            if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
-                break;
-
-            Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, fVerbose );
+            Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+            while ( 1 )
+            {
+                Abc_NtkRewrite( pNtk, 0, 0, 0 );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+                Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+                pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+            }
+            Abc_NtkMiterPrint( pNtk, "Rewriting  ", clk, pParams->fVerbose );
         }
-
-        if ( fUseFraig )
+ 
+        if ( pParams->fUseFraiging )
         {
+            int nSatFails;
             // try FRAIGing
             clk = clock();
-            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
-            Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, fVerbose );
+            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
+            Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
 //            printf( "NumFails = %d\n", nSatFails );
             if ( RetValue >= 0 )
                 break;
         }
-        else
-            nSatFails = 1000;
-
-        // increase resource limits
-//        nConfs   = ABC_MIN( nConfs * 3 / 2, 1000000000 );   // was 4/2
-        nConfs   = nSatFails * nBTLimit / 2;   
-        nImps    = ABC_MIN( nImps  * 3 / 2, 1000000000 );
-        nBTLimit = ABC_MIN( nBTLimit * 8,   1000000000 );
-
-        // timeout at 5 minutes
-//        if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC )
-//            break;
-        if ( nIter == 7 )
-            break;
     }    
-//    while ( (nConfLimit == 0 || nConfs <= nConfLimit) && 
-//            (nImpLimit  == 0 || nImps  <= nImpLimit ) );
-    while ( 1 );
 
     // try to prove it using brute force SAT
+    if ( RetValue < 0 && pParams->fUseBdds )
+    {
+        if ( pParams->fVerbose )
+        {
+            printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit );
+            fflush( stdout );
+        }
+        clk = clock();
+        pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 );
+        if ( pNtk )   
+        {
+            Abc_NtkDelete( pNtkTemp );
+            RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) );
+        }
+        else 
+            pNtk = pNtkTemp;
+        Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
+    }
+
     if ( RetValue < 0 )
     {
+        if ( pParams->fVerbose )
+        {
+            printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
+            fflush( stdout );
+        }
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 );
-        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
     }
 
     // assign the model if it was proved by rewriting (const 1 miter)
@@ -240,7 +262,8 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
 {
     if ( !fVerbose )
         return;
-    printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) );
+    printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
+        Abc_NtkIsStrash(pNtk)? Abc_AigGetLevelNum(pNtk) : Abc_NtkGetLevelNum(pNtk) );
     PRT( pString, clock() - clk );
 }
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index c968025f..9ea3ad71 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -132,6 +132,10 @@ clk = clock();
         Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
 pManRef->timeNtk += clock() - clk;
         Dec_GraphFree( pFForm );
+//    {
+//        extern int s_TotalChanges;
+//        s_TotalChanges++;
+//    }
     }
     Extra_ProgressBarStop( pProgress );
 pManRef->timeTotal = clock() - clkStart;
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 32e878b8..49208772 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -74,7 +74,7 @@ static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, C
 static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut );
 static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded );
 
-static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti );
+static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag );
 static Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose );
 static void Abc_NtkManRstStop( Abc_ManRst_t * p );
 static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
@@ -145,7 +145,7 @@ pManRst->timeCut += clock() - clk;
             break;
         // get the cuts for the given node
 clk = clock();
-        pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti ); 
+        pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti, 0 ); 
 pManRst->timeCut += clock() - clk;
 
         // perform restructuring
@@ -203,7 +203,7 @@ pManRst->timeTotal = clock() - clkStart;
 ***********************************************************************/
 void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot, int nNodesSaved )
 {
-    Abc_Obj_t * pNode, * pFanin, * pFanout;
+    Abc_Obj_t * pNode, * pFanout;//, * pFanin;
     int i, k;
     // start with the leaves
     Vec_PtrClear( p->vDecs );
@@ -276,7 +276,7 @@ Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_
 {
     Dec_Graph_t * pGraph;
     Cut_Cut_t * pCut;
-    int nCuts;
+//    int nCuts;
     p->nNodesConsidered++;
 /*
     // count the number of cuts with four inputs or more
@@ -949,7 +949,7 @@ Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd
   SeeAlso     []
 
 ***********************************************************************/
-Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti )
+Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag )
 {
     static Cut_Params_t Params, * pParams = &Params;
     Cut_Man_t * pManCut;
@@ -963,7 +963,8 @@ Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fM
     pParams->fFilter   = 1;       // filter dominated cuts
     pParams->fSeq      = 0;       // compute sequential cuts
     pParams->fDrop     = 0;       // drop cuts on the fly
-    pParams->fMulti    = fMulti;  // compute factor-cuts
+    pParams->fDag      = fDag;    // compute DAG cuts
+    pParams->fTree     = 0;       // compute tree cuts
     pParams->fVerbose  = 0;       // the verbosiness flag
     pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
     pManCut = Cut_ManStart( pParams );
@@ -1351,9 +1352,9 @@ Dec_Graph_t * Abc_NodeMffcSingleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int n
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeMffcDoubleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes )
 {
-    Dec_Graph_t * pGraph;
-    unsigned uRoot, uNode;
-    int i;
+//    Dec_Graph_t * pGraph;
+//    unsigned uRoot, uNode;
+//    int i;
 
 
     return NULL;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 71a4466f..e9de4858 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -25,6 +25,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_RS_DIV1_MAX    150   // the max number of divisors to consider
+#define ABC_RS_DIV2_MAX    500   // the max number of pair-wise divisors to consider
+
 typedef struct Abc_ManRes_t_ Abc_ManRes_t;
 struct Abc_ManRes_t_
 {
@@ -79,6 +82,7 @@ struct Abc_ManRes_t_
     int                nUsedNodeTotal;
     int                nTotalDivs;
     int                nTotalLeaves;
+    int                nTotalGain;
 };
 
 // external procedures
@@ -90,8 +94,8 @@ static void          Abc_ManResubPrint( Abc_ManRes_t * p );
 
 // other procedures
 static int           Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required );
-static int           Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves );
 static void          Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords );
+static void          Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
 
 static void          Abc_ManResubDivsS( Abc_ManRes_t * p, int Required );
 static void          Abc_ManResubDivsD( Abc_ManRes_t * p, int Required );
@@ -136,13 +140,17 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd
     // cleanup the AIG
     Abc_AigCleanup(pNtk->pManFunc);
     // start the managers
-    pManCut = Abc_NtkManCutStart( nCutMax, 10000, 100000, 100000 );
-    pManRes = Abc_ManResubStart( nCutMax, 200 );
+    pManCut = Abc_NtkManCutStart( nCutMax, 100000, 100000, 100000 );
+    pManRes = Abc_ManResubStart( nCutMax, ABC_RS_DIV1_MAX );
 
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
         Abc_NtkStartReverseLevels( pNtk );
 
+    if ( Abc_NtkLatchNum(pNtk) )
+        Abc_NtkForEachLatch(pNtk, pNode, i)
+            pNode->pNext = pNode->pData;
+
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
@@ -179,13 +187,16 @@ clk = clock();
 pManRes->timeRes += clock() - clk;
         if ( pFForm == NULL )
             continue;
+        pManRes->nTotalGain += pManRes->nLastGain;
 /*
-        if ( pNode->Id % 25 == 0 )
+        if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 )
+        {
             printf( "%6d :  L = %2d. V = %2d. Mffc = %2d. Divs = %3d.   Up = %3d. Un = %3d. B = %3d.\n", 
                    pNode->Id, pManRes->nLeaves, Abc_CutVolumeCheck(pNode, vLeaves), pManRes->nMffc, pManRes->nDivs, 
                    pManRes->vDivs1UP->nSize, pManRes->vDivs1UN->nSize, pManRes->vDivs1B->nSize );
+            Abc_ManResubPrintDivs( pManRes, pNode, vLeaves );
+        }
 */
-
         // acceptable replacement found, update the graph
 clk = clock();
         Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain );
@@ -207,6 +218,10 @@ pManRes->timeTotal = clock() - clkStart;
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->pData = NULL;
 
+    if ( Abc_NtkLatchNum(pNtk) )
+        Abc_NtkForEachLatch(pNtk, pNode, i)
+            pNode->pData = pNode->pNext, pNode->pNext = NULL;
+
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
@@ -340,6 +355,7 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
                                                    );                          PRT( "TOTAL ", p->timeTotal );
     printf( "Total leaves   = %8d.\n", p->nTotalLeaves );
     printf( "Total divisors = %8d.\n", p->nTotalDivs );
+    printf( "Total gain     = %8d.\n", p->nTotalGain );
     
 }
 
@@ -382,7 +398,7 @@ void Abc_ManResubCollectDivs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vInternal )
 ***********************************************************************/
 int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required )
 {
-    Abc_Obj_t * pNode, * pFanout;//, * pFanin;
+    Abc_Obj_t * pNode, * pFanout;
     int i, k, Limit, Counter;
 
     Vec_PtrClear( p->vDivs1UP );
@@ -451,10 +467,24 @@ Quits :
     assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
 
     assert( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) <= Vec_PtrSize(p->vSims) - p->nLeavesMax );
+    return 1;
+}
 
-/*
-if (pRoot->Id == 15281 )
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
 {
+    Abc_Obj_t * pFanin, * pNode;
+    int i, k;
     // print the nodes
     Vec_PtrForEachEntry( p->vDivs, pNode, i )
     {
@@ -488,59 +518,7 @@ if (pRoot->Id == 15281 )
     }
     printf( "\n" );
 }
-*/
 
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves )
-{
-    Abc_Obj_t * pObj;
-    int Counter, i, k;
-    // increment the traversal ID for the leaves
-    // increment the fanout counters of the leaves
-    Abc_NtkIncrementTravId( pRoot->pNtk );
-    Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves )
-    {
-        pObj->vFanouts.nSize++;
-        Abc_NodeSetTravIdCurrent( pObj ); 
-    }
-    // make sure the node is in the cone and is no one of the leaves
-    assert( Abc_NodeIsTravIdPrevious(pRoot) );
-    Counter = Abc_NodeMffcLabel( pRoot );
-    // remove the extra counters
-    Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves )
-        pObj->vFanouts.nSize--;
-
-    // sort the nodes by level!!!
-    
-    // move the labeled nodes to the end 
-    Vec_PtrClear( p->vTemp );
-    k = nLeaves;
-    Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves )
-        if ( Abc_NodeIsTravIdCurrent(pObj) )
-            Vec_PtrPush( p->vTemp, pObj );
-        else
-            Vec_PtrWriteEntry( vDivs, k++, pObj );
-    // add the labeled nodes
-    Vec_PtrForEachEntry( p->vTemp, pObj, i )
-        Vec_PtrWriteEntry( vDivs, k++, pObj );
-    assert( k == Vec_PtrSize(p->vDivs) );
-    assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
-    return Counter;
-}
 
 /**Function*************************************************************
 
@@ -928,7 +906,7 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
 
             puData1 = pObj1->pData;
 
-            if ( Vec_PtrSize(p->vDivs2UP0) < 500 )
+            if ( Vec_PtrSize(p->vDivs2UP0) < ABC_RS_DIV2_MAX )
             {
                 // get positive unate divisors
                 for ( w = 0; w < p->nWords; w++ )
@@ -965,7 +943,7 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required )
                 }
             }
 
-            if ( Vec_PtrSize(p->vDivs2UN0) < 500 )
+            if ( Vec_PtrSize(p->vDivs2UN0) < ABC_RS_DIV2_MAX )
             {
                 // get negative unate divisors
                 for ( w = 0; w < p->nWords; w++ )
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index f3360421..f11e5e9d 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -110,6 +110,10 @@ clk = clock();
             Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
 Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
             if ( fCompl ) Dec_GraphComplement( pGraph );
+//    {
+//        extern int s_TotalChanges;
+//        s_TotalChanges++;
+//    }
         }
     }
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
new file mode 100644
index 00000000..3a6a29c9
--- /dev/null
+++ b/src/base/abci/abcRr.c
@@ -0,0 +1,601 @@
+/**CFile****************************************************************
+
+  FileName    [abcRr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Redundancy removal.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_RRMan_t_ Abc_RRMan_t;
+struct Abc_RRMan_t_
+{
+    // the parameters
+    Abc_Ntk_t *      pNtk;             // the network
+    int              nFaninLevels;     // the number of fanin levels
+    int              nFanoutLevels;    // the number of fanout levels
+    // the node/fanin/fanout
+    Abc_Obj_t *      pNode;            // the node
+    Abc_Obj_t *      pFanin;           // the fanin
+    Abc_Obj_t *      pFanout;          // the fanout
+    // the intermediate cones
+    Vec_Ptr_t *      vFaninLeaves;     // the leaves of the fanin cone
+    Vec_Ptr_t *      vFanoutRoots;     // the roots of the fanout cone
+    // the window
+    Vec_Ptr_t *      vLeaves;          // the leaves of the window
+    Vec_Ptr_t *      vCone;            // the internal nodes of the window
+    Vec_Ptr_t *      vRoots;           // the roots of the window
+    Abc_Ntk_t *      pWnd;             // the window derived for the edge
+    // the miter 
+    Abc_Ntk_t *      pMiter;           // the miter derived from the window
+    Prove_Params_t * pParams;          // the miter proving parameters
+};
+
+static Abc_RRMan_t * Abc_RRManStart();
+static void          Abc_RRManStop( Abc_RRMan_t * p );
+static void          Abc_RRManClean( Abc_RRMan_t * p );
+static int           Abc_NtkRRProve( Abc_RRMan_t * p );
+static int           Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout );
+static int           Abc_NtkRRWindow( Abc_RRMan_t * p );
+
+static int           Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit );
+static int           Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout );
+static int           Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit );
+static void          Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
+static Abc_Ntk_t *   Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Removes stuck-at redundancies.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose )
+{
+    ProgressBar * pProgress;
+    Abc_RRMan_t * p;
+    Abc_Obj_t * pNode, * pFanin, * pFanout;
+    int i, k, m, nNodes;
+    // start the manager
+    p = Abc_RRManStart( nFaninLevels, nFanoutLevels );
+    p->pNtk = pNtk;
+    p->nFaninLevels  = nFaninLevels;
+    p->nFanoutLevels = nFanoutLevels;
+    // go through the nodes
+    nNodes = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodes );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // stop if all nodes have been tried once
+        if ( i >= nNodes )
+            break;
+        // skip the constant node
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        // skip the nodes with many fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1000 )
+            continue;
+        // construct the window
+        if ( !fUseFanouts )
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+            {
+                Abc_RRManClean( p );
+                p->pNode   = pNode;
+                p->pFanin  = pFanin;
+                p->pFanout = NULL;
+                if ( !Abc_NtkRRWindow( p ) )
+                    continue;
+                if ( !Abc_NtkRRProve( p ) )
+                    continue;
+                Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
+                break;
+            }
+            continue;
+        }
+        // use the fanouts
+        Abc_ObjForEachFanout( pNode, pFanout, m )
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            Abc_RRManClean( p );
+            p->pNode   = pNode;
+            p->pFanin  = pFanin;
+            p->pFanout = pFanout;
+            if ( !Abc_NtkRRWindow( p ) )
+                continue;
+            if ( !Abc_NtkRRProve( p ) )
+                continue;
+            Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
+            break;
+        }
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_RRManStop( p );
+    // put the nodes into the DFS order and reassign their IDs
+    Abc_NtkReassignIds( pNtk );
+    Abc_NtkGetLevelNum( pNtk );
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkRR: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_RRMan_t * Abc_RRManStart()
+{
+    Abc_RRMan_t * p;
+    p = ALLOC( Abc_RRMan_t, 1 );
+    memset( p, 0, sizeof(Abc_RRMan_t) );
+    p->vFaninLeaves  = Vec_PtrAlloc( 100 );  // the leaves of the fanin cone
+    p->vFanoutRoots  = Vec_PtrAlloc( 100 );  // the roots of the fanout cone
+    p->vLeaves       = Vec_PtrAlloc( 100 );  // the leaves of the window
+    p->vCone         = Vec_PtrAlloc( 100 );  // the internal nodes of the window
+    p->vRoots        = Vec_PtrAlloc( 100 );  // the roots of the window
+    p->pParams       = ALLOC( Prove_Params_t, 1 );
+    memset( p->pParams, 0, sizeof(Prove_Params_t) );
+    Prove_ParamsSetDefault( p->pParams );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RRManStop( Abc_RRMan_t * p )
+{
+    Abc_RRManClean( p );
+    Vec_PtrFree( p->vFaninLeaves  );  
+    Vec_PtrFree( p->vFanoutRoots  );  
+    Vec_PtrFree( p->vLeaves );  
+    Vec_PtrFree( p->vCone );  
+    Vec_PtrFree( p->vRoots );  
+    free( p->pParams );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clean the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RRManClean( Abc_RRMan_t * p )
+{
+    p->pNode   = NULL; 
+    p->pFanin  = NULL; 
+    p->pFanout = NULL; 
+    Vec_PtrClear( p->vFaninLeaves  );  
+    Vec_PtrClear( p->vFanoutRoots  );  
+    Vec_PtrClear( p->vLeaves );  
+    Vec_PtrClear( p->vCone );  
+    Vec_PtrClear( p->vRoots );  
+    if ( p->pWnd )   Abc_NtkDelete( p->pWnd );
+    if ( p->pMiter ) Abc_NtkDelete( p->pMiter );
+    p->pWnd   = NULL;
+    p->pMiter = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the miter is constant 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRRProve( Abc_RRMan_t * p )
+{
+    Abc_Ntk_t * pWndCopy;
+    int RetValue;
+    pWndCopy = Abc_NtkDup( p->pWnd );
+    Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy, p->pFanin->pCopy, p->pFanout? p->pFanout->pCopy : NULL );
+    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1 );
+    RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );
+    if ( RetValue == 1 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the network after redundancy removal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout )
+{
+    Abc_Obj_t * pNodeNew, * pFanoutNew;
+    assert( pFanout == NULL );
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( !Abc_ObjIsComplement(pFanin) );
+    assert( !Abc_ObjIsComplement(pFanout) );
+    // find the node after redundancy removal
+    if ( pFanin == Abc_ObjFanin0(pNode) )
+        pNodeNew = Abc_ObjChild1(pNode);
+    else if ( pFanin == Abc_ObjFanin1(pNode) )
+        pNodeNew = Abc_ObjChild0(pNode);
+    else assert( 0 );
+    // replace
+    if ( pFanout == NULL )
+    {
+        Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew, 0 );
+        return 1;
+    }
+    // find the fanout after redundancy removal
+    if ( pNode == Abc_ObjFanin0(pFanout) )
+        pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );
+    else if ( pNode == Abc_ObjFanin1(pFanout) )
+        pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) );
+    else assert( 0 );
+    // replace
+    Abc_AigReplace( pNtk->pManFunc, pFanout, pFanoutNew, 0 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs window for checking RR.]
+
+  Description [If the window (p->pWnd) with the given scope (p->nFaninLevels, 
+  p->nFanoutLevels) cannot be constructed, returns 0. Otherwise, returns 1.
+  The levels are measured from the fanin node (pFanin) and the fanout node
+  (pEdgeFanout), respectively.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRRWindow( Abc_RRMan_t * p )
+{
+    Abc_Obj_t * pObj, * pFanout, * pEdgeFanin, * pEdgeFanout;
+    int i, k;
+
+    // get the edge
+    pEdgeFanout = p->pFanout? p->pFanout : p->pNode;
+    pEdgeFanin  = p->pFanout? p->pNode : p->pFanin;
+
+    // start the TFI leaves with the fanin
+    Abc_NtkIncrementTravId( p->pNtk );
+    Abc_NodeSetTravIdCurrent( p->pFanin );
+    Vec_PtrPush( p->vFaninLeaves, p->pFanin );
+    // mark the TFI cone and collect the leaves down to the given level
+    while ( Abc_NtkRRTfi_int(p->vFaninLeaves, p->pFanin->Level - p->nFaninLevels) );
+
+    // collect the TFO cone of the leaves
+    Abc_NtkIncrementTravId( p->pNtk );
+    Vec_PtrForEachEntry( p->vFaninLeaves, pObj, i )
+    {
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+        {
+            if ( !Abc_ObjIsNode(pFanout) )
+                continue;
+            if ( pFanout->Level > pEdgeFanout->Level + p->nFanoutLevels )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pFanout );
+            Vec_PtrPush( p->vFanoutRoots, pFanout );
+        }
+    }
+    // mark the TFO cone and collect the leaves up to the given level (while skipping the edge)
+    while ( Abc_NtkRRTfo_int(p->vFanoutRoots, pEdgeFanout->Level + p->nFanoutLevels, pEdgeFanin, pEdgeFanout) );
+    // unmark the nodes
+    Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
+        pObj->fMarkA = 0;
+
+    // mark the current roots
+    Abc_NtkIncrementTravId( p->pNtk );
+    Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );
+    // collect roots reachable from the fanout (p->vRoots)
+    if ( !Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, pEdgeFanout->Level + p->nFanoutLevels + 5 ) )
+        return 0;
+
+    // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves)
+    // using the previous marks coming from the TFO cone
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone );
+    // unmark the nodes
+    Vec_PtrForEachEntry( p->vCone, pObj, i )
+        pObj->fMarkA = 0;
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        pObj->fMarkA = 0;
+
+    // create a new network
+    p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes in the TFI and collects their leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit )
+{
+    Abc_Obj_t * pObj, * pNext;
+    int i, k, LevelMax, nSize;
+    // find the maximum level of leaves
+    LevelMax = 0;
+    Vec_PtrForEachEntry( vFaninLeaves, pObj, i )
+        if ( LevelMax < (int)pObj->Level )
+            LevelMax = pObj->Level;
+    // if the nodes are all PIs, LevelMax == 0
+    if ( LevelMax == 0 || LevelMax <= LevelLimit )
+        return 0;
+    // expand the nodes with the minimum level
+    nSize = Vec_PtrSize(vFaninLeaves);
+    Vec_PtrForEachEntryStop( vFaninLeaves, pObj, i, nSize )
+    {
+        if ( LevelMax != (int)pObj->Level )
+            continue;
+        Abc_ObjForEachFanin( pObj, pNext, k )
+        {
+            if ( Abc_NodeIsTravIdCurrent(pNext) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNext );
+            Vec_PtrPush( vFaninLeaves, pNext );
+        }
+    }
+    // remove old nodes (cannot remove a PI)
+    k = 0;
+    Vec_PtrForEachEntry( vFaninLeaves, pObj, i )
+    {
+        if ( LevelMax == (int)pObj->Level )
+            continue;
+        Vec_PtrWriteEntry( vFaninLeaves, k++, pObj );
+    }
+    Vec_PtrShrink( vFaninLeaves, k );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes in the TFO and collects their roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout )
+{
+    Abc_Obj_t * pObj, * pNext;
+    int i, k, LevelMin, nSize;
+    // find the minimum level of roots
+    LevelMin = ABC_INFINITY;
+    Vec_PtrForEachEntry( vFanoutRoots, pObj, i )
+        if ( Abc_ObjIsNode(pObj) && !pObj->fMarkA && LevelMin > (int)pObj->Level )
+            LevelMin = pObj->Level;
+    // if the nodes are all POs, LevelMin == ABC_INFINITY
+    if ( LevelMin == ABC_INFINITY || LevelMin > LevelLimit )
+        return 0;
+    // expand the nodes with the minimum level
+    nSize = Vec_PtrSize(vFanoutRoots);
+    Vec_PtrForEachEntryStop( vFanoutRoots, pObj, i, nSize )
+    {
+        if ( LevelMin != (int)pObj->Level )
+            continue;
+        Abc_ObjForEachFanout( pObj, pNext, k )
+        {
+            if ( !Abc_ObjIsNode(pNext) || pNext->Level > (unsigned)LevelLimit )
+            {
+                pObj->fMarkA = 1;
+                continue;
+            }
+            if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent(pNext) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNext );
+            Vec_PtrPush( vFanoutRoots, pNext );
+        }
+    }
+    // remove old nodes
+    k = 0;
+    Vec_PtrForEachEntry( vFanoutRoots, pObj, i )
+    {
+        if ( LevelMin == (int)pObj->Level )
+        {
+            // check if the node has external fanouts
+            Abc_ObjForEachFanout( pObj, pNext, k )
+            {
+                if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
+                    continue;
+                if ( !Abc_NodeIsTravIdCurrent(pNext) )
+                    break;
+            }
+            // if external fanout is found, do not remove the node
+            if ( pNext )
+                continue;
+        }
+        Vec_PtrWriteEntry( vFanoutRoots, k++, pObj );
+    }
+    Vec_PtrShrink( vFanoutRoots, k );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the roots in the TFO of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit )
+        return 0;
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+    {
+        Vec_PtrPushUnique( vRoots, pNode );
+        return 1;
+    }
+    Abc_NodeSetTravIdCurrent( pNode );
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    // skip visited nodes
+    if ( pNode->fMarkA )
+        return;
+    pNode->fMarkA = 1;
+    // add the node if it was not visited in the previus run
+    if ( !Abc_NodeIsTravIdPrevious(pNode) )
+    {
+        Vec_PtrPush( vLeaves, pNode );
+        return;
+    }
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone );
+    Vec_PtrPush( vCone, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav( "temp" );
+    // map the constant nodes
+    if ( Abc_NtkConst1(pNtk) )
+        Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    // create and map the PIs
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->pCopy = Abc_NtkCreatePi(pNtkNew);
+    // copy the AND gates
+    Vec_PtrForEachEntry( vCone, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // compare the number of nodes before and after
+    if ( Vec_PtrSize(vCone) != Abc_NtkNodeNum(pNtkNew) )
+        printf( "Warning: Structural hashing during windowing reduced %d nodes (this is a bug).\n",
+            Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) );
+    // create the POs
+    Vec_PtrForEachEntry( vRoots, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy );
+    // add the PI/PO names
+    Abc_NtkAddDummyPiNames( pNtkNew );
+    Abc_NtkAddDummyPoNames( pNtkNew );
+    // check
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkWindow: The network check has failed.\n" );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index f7400313..9348231b 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
 static nMuxes;
 
 ////////////////////////////////////////////////////////////////////////
@@ -42,7 +42,7 @@ static nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose )
 {
     solver * pSat;
     lbool   status;
@@ -56,7 +56,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbo
 
     // load clauses into the solver
     clk = clock();
-    pSat = Abc_NtkMiterSatCreate( pNtk );
+    pSat = Abc_NtkMiterSatCreate( pNtk, fJFront );
     if ( pSat == NULL )
         return 1;
 //    printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
@@ -107,6 +107,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbo
         Vec_IntFree( vCiIds );
     }
     // free the solver
+    if ( fVerbose )
+        Asat_SatPrintStats( stdout, pSat );
     solver_delete( pSat );
     return RetValue;
 }
@@ -391,12 +393,14 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
+int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
 {
     Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
     Vec_Ptr_t * vNodes, * vSuper;
-    Vec_Int_t * vVars;
+    Vec_Int_t * vVars, * vFanio;
+    Vec_Vec_t * vCircuit;
     int i, k, fUseMuxes = 1;
+    int clk1 = clock(), clk;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -408,6 +412,9 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
     vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
     vVars  = Vec_IntAlloc( 100 );    // the temporary array for variables in the clause
+    if ( fJFront )
+        vCircuit = Vec_VecAlloc( 1000 );
+//        vCircuit = Vec_VecStart( 184 );
 
     // add the clause for the constant node
     pNode = Abc_NtkConst1(pNtk);
@@ -485,6 +492,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
             if ( vSuper->nSize == 0 )
             {
                 if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
+//                if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
                     return 0;
             }
             else
@@ -493,6 +501,32 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
                     return 0;
             }
         }
+        // add the variables to the J-frontier
+        if ( !fJFront )
+            continue;
+        // make sure that the fanin entries go first
+        assert( pNode->pCopy );
+        Vec_VecExpand( vCircuit, (int)pNode->pCopy );
+        vFanio = Vec_VecEntry( vCircuit, (int)pNode->pCopy );
+        Vec_PtrForEachEntryReverse( vSuper, pFanin, k )
+//        Vec_PtrForEachEntry( vSuper, pFanin, k )
+        {
+            pFanin = Abc_ObjRegular( pFanin );
+            assert( pFanin->pCopy && pFanin->pCopy != pNode->pCopy );
+            Vec_IntPushFirst( vFanio, (int)pFanin->pCopy );
+            Vec_VecPush( vCircuit, (int)pFanin->pCopy, pNode->pCopy );
+        }
+    }
+
+    // create the variable order
+    if ( fJFront )
+    {
+    clk = clock();
+        Asat_JManStart( pSat, vCircuit );
+        Vec_VecFree( vCircuit );
+    PRT( "Setup", clock() - clk );
+//        Asat_JManStop( pSat );
+//    PRT( "Total", clock() - clk1 );
     }
 
     // delete
@@ -513,7 +547,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront )
 {
     solver * pSat;
     Abc_Obj_t * pNode;
@@ -522,7 +556,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     nMuxes = 0;
 
     pSat = solver_new();
-    RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
+    RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront );
     Abc_NtkForEachObj( pNtk, pNode, i )
         pNode->fMarkA = 0;
 //    Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index fbaca324..cfbd4694 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -58,7 +58,13 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
@@ -72,7 +78,9 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 //    if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
 //        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
     if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
-        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    {
+//        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    }
     // duplicate EXDC 
     if ( pNtk->pExdc )
         pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
@@ -108,7 +116,13 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
     if ( Abc_NtkIsBddLogic(pNtk2) )
-        Abc_NtkBddToSop(pNtk2, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk2, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return 0;
+        }
+    }
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )
@@ -163,6 +177,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes
         assert( pObj->pCopy == NULL );
         // mark the old object with the new AIG node
         pObj->pCopy = pNodeNew;
+        Abc_HManAddProto( pObj->pCopy, pObj );
     }
     Vec_PtrFree( vNodes );
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 35cf896f..fad3bd92 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0 );
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0, 1, fVerbose );
     Cudd_AutodynDisable( dd );
     Cudd_zddVarsFromBddVars( dd, 2 );
 clkBdd = clock() - clk;
diff --git a/src/base/abci/abcTrace.c b/src/base/abci/abcTrace.c
new file mode 100644
index 00000000..0275c0a1
--- /dev/null
+++ b/src/base/abci/abcTrace.c
@@ -0,0 +1,804 @@
+/**CFile****************************************************************
+
+  FileName    [abcHistory.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcHistory.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+#define ABC_SIM_VARS   16    // the max number of variables in the cone
+#define ABC_SIM_OBJS  200    // the max number of objects in the cone
+
+typedef struct Abc_HMan_t_ Abc_HMan_t;
+typedef struct Abc_HObj_t_ Abc_HObj_t;
+typedef struct Abc_HNum_t_ Abc_HNum_t;
+
+struct Abc_HNum_t_
+{
+    unsigned         fCompl :  1;  // set to 1 if the node is complemented
+    unsigned         NtkId  :  6;  // the network ID 
+    unsigned         ObjId  : 24;  // the node ID 
+};
+
+struct Abc_HObj_t_
+{
+    // object info
+    unsigned         fProof :  1;  // set to 1 if the node is proved
+    unsigned         fPhase :  1;  // set to 1 if the node's phase differs from Old
+    unsigned         fPi    :  1;  // the node is a PI
+    unsigned         fPo    :  1;  // the node is a PO
+    unsigned         fConst :  1;  // the node is a constant
+    unsigned         fVisited: 1;  // the flag shows if the node is visited
+    unsigned         NtkId  : 10;  // the network ID
+    unsigned         Num    : 16;  // a temporary number
+    // history record
+    Abc_HNum_t       Fan0;         // immediate fanin
+    Abc_HNum_t       Fan1;         // immediate fanin
+    Abc_HNum_t       Proto;        // old node if present
+//    Abc_HNum_t       Equ;          // equiv node if present
+};
+
+struct Abc_HMan_t_
+{
+    // storage for history information
+    Vec_Vec_t *      vNtks;        // the history nodes belonging to each network
+    Vec_Int_t *      vProof;       // flags showing if the network is proved
+    // storage for simulation info
+    int              nVarsMax;     // the max number of cone leaves
+    int              nObjsMax;     // the max number of cone nodes
+    Vec_Ptr_t *      vObjs;        // the cone nodes
+    int              nBits;        // the number of simulation bits
+    int              nWords;       // the number of unsigneds for siminfo
+    int              nWordsCur;    // the current number of words
+    Vec_Ptr_t *      vSims;        // simulation info
+    unsigned *       pInfo;        // pointer to simulation info
+    // other info
+    Vec_Ptr_t *      vCone0;
+    Vec_Ptr_t *      vCone1;
+    // memory manager
+    Extra_MmFixed_t* pMmObj;       // memory manager for objects
+};
+
+static Abc_HMan_t * s_pHMan = NULL;
+
+static inline int          Abc_HObjProof( Abc_HObj_t * p )   { return p->fProof; }
+static inline int          Abc_HObjPhase( Abc_HObj_t * p )   { return p->fPhase; }
+static inline int          Abc_HObjPi   ( Abc_HObj_t * p )   { return p->fPi;    }
+static inline int          Abc_HObjPo   ( Abc_HObj_t * p )   { return p->fPo;    }
+static inline int          Abc_HObjConst( Abc_HObj_t * p )   { return p->fConst; }
+static inline int          Abc_HObjNtkId( Abc_HObj_t * p )   { return p->NtkId;  }
+static inline int          Abc_HObjNum  ( Abc_HObj_t * p )   { return p->Num;    }
+static inline Abc_HObj_t * Abc_HObjFanin0( Abc_HObj_t * p )  { return !p->Fan0.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Fan0.NtkId),  p->Fan0.ObjId ); }
+static inline Abc_HObj_t * Abc_HObjFanin1( Abc_HObj_t * p )  { return !p->Fan1.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Fan1.NtkId),  p->Fan1.ObjId ); }
+static inline Abc_HObj_t * Abc_HObjProto ( Abc_HObj_t * p )  { return !p->Proto.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Proto.NtkId), p->Proto.ObjId ); }
+static inline int          Abc_HObjFaninC0( Abc_HObj_t * p ) { return p->Fan0.fCompl; }
+static inline int          Abc_HObjFaninC1( Abc_HObj_t * p ) { return p->Fan1.fCompl; }
+
+static inline Abc_HObj_t * Abc_ObjHObj( Abc_Obj_t * p )      { return Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->pNtk->Id),  p->Id ); }
+
+static int Abc_HManVerifyPair( int NtkIdOld, int NtkIdNew );
+static int Abc_HManVerifyNodes_rec( Abc_HObj_t * pHOld, Abc_HObj_t * pHNew );
+
+static Vec_Ptr_t * Abc_HManCollectLeaves( Abc_HObj_t * pHNew );
+static Vec_Ptr_t * Abc_HManCollectCone( Abc_HObj_t * pHOld, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
+static int Abc_HManSimulate( Vec_Ptr_t * vCone0, Vec_Ptr_t * vCone1, int nLeaves, int * pPhase );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManStart()
+{
+    Abc_HMan_t * p;
+    unsigned * pData;
+    int i, k;
+    assert( s_pHMan == NULL );
+    assert( sizeof(unsigned) == 4 );
+    // allocate manager
+    p = ALLOC( Abc_HMan_t, 1 );
+    memset( p, 0, sizeof(Abc_HMan_t) );
+    // allocate storage for all nodes
+    p->vNtks  = Vec_VecStart( 1 );
+    p->vProof = Vec_IntStart( 1 );
+    // allocate temporary storage for objects
+    p->nVarsMax = ABC_SIM_VARS;
+    p->nObjsMax = ABC_SIM_OBJS;
+    p->vObjs    = Vec_PtrAlloc( p->nObjsMax );
+    // allocate simulation info
+    p->nBits    = (1 << p->nVarsMax);
+    p->nWords   = (p->nBits <= 32)? 1 : (p->nBits / 32);
+    p->pInfo    = ALLOC( unsigned, p->nWords * p->nObjsMax );
+    memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nVarsMax );
+    p->vSims    = Vec_PtrAlloc( p->nObjsMax );
+    for ( i = 0; i < p->nObjsMax; i++ )
+        Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords );
+    // set elementary truth tables
+    for ( k = 0; k < p->nVarsMax; k++ )
+    {
+        pData = p->vSims->pArray[k];
+        for ( i = 0; i < p->nBits; i++ )
+            if ( i & (1 << k) )
+                pData[i/32] |= (1 << (i%32));
+    }
+    // allocate storage for the nodes
+    p->pMmObj = Extra_MmFixedStart( sizeof(Abc_HObj_t) );
+    p->vCone0 = Vec_PtrAlloc( p->nObjsMax );
+    p->vCone1 = Vec_PtrAlloc( p->nObjsMax );
+    s_pHMan = p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManStop()
+{
+    assert( s_pHMan != NULL );
+    Extra_MmFixedStop( s_pHMan->pMmObj, 0 );
+    Vec_PtrFree( s_pHMan->vObjs );
+    Vec_PtrFree( s_pHMan->vSims );
+    Vec_VecFree( s_pHMan->vNtks );
+    Vec_IntFree( s_pHMan->vProof );
+    Vec_PtrFree( s_pHMan->vCone0 );
+    Vec_PtrFree( s_pHMan->vCone1 );
+    free( s_pHMan->pInfo );
+    free( s_pHMan );
+    s_pHMan = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManIsRunning()
+{
+    return s_pHMan != NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when a new network is created.]
+
+  Description [Returns the new ID for the network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManGetNewNtkId()
+{
+    if ( s_pHMan == NULL )
+        return 0;
+    return Vec_VecSize( s_pHMan->vNtks );  // what if the new network has no nodes?
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when the object is created.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManAddObj( Abc_Obj_t * pObj )
+{
+    Abc_HObj_t * pHObj;
+    if ( s_pHMan == NULL )
+        return;
+    pHObj = (Abc_HObj_t *)Extra_MmFixedEntryFetch( s_pHMan->pMmObj );
+    memset( pHObj, 0, sizeof(Abc_HObj_t) );
+    // set the object type
+    pHObj->NtkId = pObj->pNtk->Id;
+    if ( Abc_ObjIsCi(pObj) )
+        pHObj->fPi = 1;
+    else if ( Abc_ObjIsCo(pObj) )
+        pHObj->fPo = 1;
+    Vec_VecPush( s_pHMan->vNtks, pObj->pNtk->Id, pHObj );
+    // set the proof parameter for the network
+    if ( Vec_IntSize( s_pHMan->vProof ) == pObj->pNtk->Id )
+        Vec_IntPush( s_pHMan->vProof, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when the fanin is added to the object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
+{
+    Abc_HObj_t * pHObj;
+    int fCompl;
+    if ( s_pHMan == NULL )
+        return;
+    // take off the complemented attribute
+    assert( !Abc_ObjIsComplement(pObj) );
+    fCompl = Abc_ObjIsComplement(pFanin);
+    pFanin = Abc_ObjRegular(pFanin);
+    // add the fanin
+    assert( pObj->pNtk == pFanin->pNtk );
+    pHObj = Abc_ObjHObj(pObj);
+    if ( pHObj->Fan0.NtkId == 0 )
+    {
+        pHObj->Fan0.NtkId = pFanin->pNtk->Id;
+        pHObj->Fan0.ObjId = pFanin->Id;
+        pHObj->Fan0.fCompl = fCompl;
+    }
+    else if ( pHObj->Fan1.NtkId == 0 )
+    {
+        pHObj->Fan1.NtkId = pFanin->pNtk->Id;
+        pHObj->Fan1.ObjId = pFanin->Id;
+        pHObj->Fan1.fCompl = fCompl;
+    }
+    else assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when the fanin's input should be complemented.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManXorFaninC( Abc_Obj_t * pObj, int iFanin )
+{
+    Abc_HObj_t * pHObj;
+    if ( s_pHMan == NULL )
+        return;
+    assert( iFanin < 2 );
+    pHObj = Abc_ObjHObj(pObj);
+    if ( iFanin == 0 )
+        pHObj->Fan0.fCompl ^= 1;
+    else if ( iFanin == 1 )
+        pHObj->Fan1.fCompl ^= 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when the fanin is added to the object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManRemoveFanins( Abc_Obj_t * pObj )
+{
+    Abc_HObj_t * pHObj;
+    if ( s_pHMan == NULL )
+        return;
+    assert( !Abc_ObjIsComplement(pObj) );
+    pHObj = Abc_ObjHObj(pObj);
+    pHObj->Fan0.NtkId = 0;
+    pHObj->Fan0.ObjId = 0;
+    pHObj->Fan0.fCompl = 0;
+    pHObj->Fan1.NtkId = 0;
+    pHObj->Fan1.ObjId = 0;
+    pHObj->Fan1.fCompl = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when a new prototype of the old object is set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManAddProto( Abc_Obj_t * pObj, Abc_Obj_t * pProto )
+{
+    Abc_HObj_t * pHObj;
+    if ( s_pHMan == NULL )
+        return;
+    // ignore polarity for now
+    pObj   = Abc_ObjRegular(pObj);
+    pProto = Abc_ObjRegular(pProto);
+    // set the prototype
+    assert( pObj->pNtk != pProto->pNtk );
+    if ( pObj->pNtk->Id == 0 )
+        return;
+    pHObj = Abc_ObjHObj(pObj);
+    pHObj->Proto.NtkId = pProto->pNtk->Id;
+    pHObj->Proto.ObjId = pProto->Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Called when an equivalent node is created.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManMapAddEqu( Abc_Obj_t * pObj, Abc_Obj_t * pEqu )
+{
+/*
+    Abc_HObj_t * pHObj;
+    if ( s_pHMan == NULL )
+        return;
+    // ignore polarity for now
+    pObj  = Abc_ObjRegular(pObj);
+    pEqu  = Abc_ObjRegular(pEqu);
+    // set the equivalent node
+    assert( pObj->pNtk == pEqu->pNtk );
+    pHObj = Abc_ObjHObj(pObj);
+    Abc_ObjHObj(pObj)->Equ.NtkId = pEqu->pNtk->Id;
+    Abc_ObjHObj(pObj)->Equ.ObjId = pEqu->Id;
+*/
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the verification procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManPopulate( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    if ( !Abc_NtkIsStrash(pNtk) )
+        return 0;
+    // allocate the network ID
+    pNtk->Id = Abc_HManGetNewNtkId();
+    assert( pNtk->Id == 1 );
+    // create the objects
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        Abc_HManAddObj( pObj );
+        if ( Abc_ObjFaninNum(pObj) > 0 )
+            Abc_HManAddFanin( pObj, Abc_ObjChild0(pObj) );
+        if ( Abc_ObjFaninNum(pObj) > 1 )
+            Abc_HManAddFanin( pObj, Abc_ObjChild1(pObj) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [The main verification procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManVerify( int NtkIdOld, int NtkIdNew )
+{
+    int i;
+    // prove the equality pairwise
+    for ( i = NtkIdOld; i < NtkIdNew; i++ )
+    {
+        if ( Vec_IntEntry(s_pHMan->vProof, i) )
+            continue;
+        if ( !Abc_HManVerifyPair( i, i+1 ) )
+            return 0;
+        Vec_IntWriteEntry( s_pHMan->vProof, i, 1 );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies two networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManVerifyPair( int NtkIdOld, int NtkIdNew )
+{
+    Vec_Ptr_t * vNtkNew, * vNtkOld, * vPosNew;
+    Abc_HObj_t * pHObj;
+    int i;
+    // get hold of the network nodes
+    vNtkNew = Vec_VecEntry( s_pHMan->vNtks, NtkIdNew );
+    vNtkOld = Vec_VecEntry( s_pHMan->vNtks, NtkIdOld );
+    Vec_PtrForEachEntry( vNtkNew, pHObj, i )
+        pHObj->fVisited = 0;
+    Vec_PtrForEachEntry( vNtkOld, pHObj, i )
+        pHObj->fVisited = 0;
+    // collect new POs
+    vPosNew = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( vNtkNew, pHObj, i )
+        if ( pHObj->fPo )
+            Vec_PtrPush( vPosNew, pHObj );
+    // prove them recursively (assuming PO ordering is the same)
+    Vec_PtrForEachEntry( vPosNew, pHObj, i )
+    {
+        if ( Abc_HObjProto(pHObj) == NULL )
+        {
+            printf( "History: PO %d has no prototype\n", i ); 
+            return 0;
+        }
+        if ( !Abc_HManVerifyNodes_rec( Abc_HObjProto(pHObj), pHObj ) )
+        {
+            printf( "History: Verification failed for outputs of PO pair number %d\n", i ); 
+            return 0;
+        }
+    }
+    printf( "History: Verification succeeded.\n" ); 
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively verifies two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManVerifyNodes_rec( Abc_HObj_t * pHOld, Abc_HObj_t * pHNew )
+{
+    Vec_Ptr_t * vLeaves;
+    Abc_HObj_t * pHObj, * pHPro0, * pHPro1;
+    int i, fPhase;
+
+    assert( Abc_HObjProto(pHNew) == pHOld );
+    if ( pHNew->fProof )
+        return 1;
+    pHNew->fProof = 1;
+    // consider simple cases
+    if ( pHNew->fPi || pHNew->fConst )
+        return 1;
+    if ( pHNew->fPo )
+    {
+        if ( !Abc_HManVerifyNodes_rec( Abc_HObjFanin0(pHOld), Abc_HObjFanin0(pHNew) ) )
+            return 0;
+        if ( (Abc_HObjFaninC0(pHOld) ^ Abc_HObjFaninC0(pHNew)) != (int)pHNew->fPhase )
+        {
+            printf( "History: Phase of PO nodes does not agree.\n" );
+            return 0;
+        }
+        return 1;
+    }
+    // the elementary node
+    pHPro0 = Abc_HObjProto( Abc_HObjFanin0(pHNew) );
+    pHPro1 = Abc_HObjProto( Abc_HObjFanin1(pHNew) );
+    if ( pHPro0 && pHPro1 )
+    {
+        if ( !Abc_HManVerifyNodes_rec( pHPro0, Abc_HObjFanin0(pHNew) ) )
+            return 0;
+        if ( !Abc_HManVerifyNodes_rec( pHPro1, Abc_HObjFanin1(pHNew) ) )
+            return 0;
+        if ( Abc_HObjFanin0(pHOld) != pHPro0 || Abc_HObjFanin1(pHOld) != pHPro1 )
+        {
+            printf( "History: Internal node does not match.\n" );
+            return 0;
+        }
+        if ( Abc_HObjFaninC0(pHOld) != Abc_HObjFaninC0(pHNew) ||
+             Abc_HObjFaninC1(pHOld) != Abc_HObjFaninC1(pHNew) )
+        {
+            printf( "History: Phase of internal node does not match.\n" );
+            return 0;
+        }
+        return 1;
+    }
+    // collect the leaves
+    vLeaves = Abc_HManCollectLeaves( pHNew );
+    if ( Vec_PtrSize(vLeaves) > 16 )
+    {
+        printf( "History: The bound on the number of inputs is exceeded.\n" );
+        return 0;
+    }
+    s_pHMan->nWordsCur = ((1 << Vec_PtrSize(vLeaves)) <= 32)? 1 : ((1 << Vec_PtrSize(vLeaves)) / 32);
+    // prove recursively
+    Vec_PtrForEachEntry( vLeaves, pHObj, i )
+        if ( !Abc_HManVerifyNodes_rec( Abc_HObjProto(pHObj), pHObj ) )
+        {
+            Vec_PtrFree( vLeaves );
+            return 0;
+        }
+    // get the first node
+    Abc_HManCollectCone( pHNew, vLeaves, s_pHMan->vCone1 );
+    if ( Vec_PtrSize(s_pHMan->vCone1) > ABC_SIM_OBJS - ABC_SIM_VARS - 1 )
+    {
+        printf( "History: The bound on the number of cone nodes is exceeded.\n" );
+        return 0;
+    }
+    // get the second cone
+    Vec_PtrForEachEntry( vLeaves, pHObj, i )
+        Vec_PtrWriteEntry( vLeaves, i, Abc_HObjProto(pHObj) );
+    Abc_HManCollectCone( pHOld, vLeaves, s_pHMan->vCone0 );
+    if ( Vec_PtrSize(s_pHMan->vCone0) > ABC_SIM_OBJS - ABC_SIM_VARS - 1 )
+    {
+        printf( "History: The bound on the number of cone nodes is exceeded.\n" );
+        return 0;
+    }
+    // compare the truth tables
+    if ( !Abc_HManSimulate( s_pHMan->vCone0, s_pHMan->vCone1, Vec_PtrSize(vLeaves), &fPhase ) )
+    {
+        Vec_PtrFree( vLeaves );
+        printf( "History: Verification failed at an internal node.\n" );
+        return 0;
+    }
+    printf( "Succeeded.\n" );
+    pHNew->fPhase = fPhase;
+    Vec_PtrFree( vLeaves );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the leaves of the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManCollectLeaves_rec( Abc_HObj_t * pHNew, Vec_Ptr_t * vLeaves )
+{
+    Abc_HObj_t * pHPro;
+    if ( pHPro = Abc_HObjProto( pHNew ) )
+    {
+        Vec_PtrPushUnique( vLeaves, pHNew );
+        return;
+    }
+    assert( !pHNew->fPi && !pHNew->fPo && !pHNew->fConst );
+    Abc_HManCollectLeaves_rec( Abc_HObjFanin0(pHNew), vLeaves );
+    Abc_HManCollectLeaves_rec( Abc_HObjFanin1(pHNew), vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the leaves of the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_HManCollectLeaves( Abc_HObj_t * pHNew )
+{
+    Vec_Ptr_t * vLeaves;
+    vLeaves = Vec_PtrAlloc( 100 );
+    Abc_HManCollectLeaves_rec( Abc_HObjFanin0(pHNew), vLeaves );
+    Abc_HManCollectLeaves_rec( Abc_HObjFanin1(pHNew), vLeaves );
+    return vLeaves;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManCollectCone_rec( Abc_HObj_t * pHObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+{
+    if ( pHObj->fVisited )
+        return;
+    pHObj->fVisited = 1;
+    assert( !pHObj->fPi && !pHObj->fPo && !pHObj->fConst );
+    Abc_HManCollectCone_rec( Abc_HObjFanin0(pHObj), vLeaves, vCone );
+    Abc_HManCollectCone_rec( Abc_HObjFanin1(pHObj), vLeaves, vCone );
+    pHObj->Num = Vec_PtrSize(vCone);
+    Vec_PtrPush( vCone, pHObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_HManCollectCone( Abc_HObj_t * pHRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+{
+    Abc_HObj_t * pHObj;
+    int i;
+    Vec_PtrClear( vCone );
+    Vec_PtrForEachEntry( vLeaves, pHObj, i )
+    {
+        pHObj->fVisited = 1;
+        pHObj->Num = Vec_PtrSize(vCone);
+        Vec_PtrPush( vCone, pHObj );
+    }
+    Abc_HManCollectCone_rec( Abc_HObjFanin0(pHRoot), vLeaves, vCone );
+    Abc_HManCollectCone_rec( Abc_HObjFanin1(pHRoot), vLeaves, vCone );
+    return vCone;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_HManSimulateOne( Vec_Ptr_t * vCone, int nLeaves, int fUsePhase )
+{
+    Abc_HObj_t * pHObj, * pHFan0, * pHFan1;
+    unsigned * puData0, * puData1, * puData;
+    int k, i, fComp0, fComp1;
+    // set the leaves
+    Vec_PtrForEachEntryStart( vCone, pHObj, i, nLeaves )
+    {
+        pHFan0  = Abc_HObjFanin0(pHObj);
+        pHFan1  = Abc_HObjFanin1(pHObj);
+        // consider the case of interver or buffer
+        if ( pHFan1 == NULL )
+        {
+            puData  = Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+i-nLeaves);
+            puData0 = ((int)pHFan0->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan0->Num) : 
+                                                    Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan0->Num-nLeaves);
+            fComp0 = Abc_HObjFaninC0(pHObj) ^ (fUsePhase && (int)pHFan0->Num < nLeaves && pHFan0->fPhase);
+            if ( fComp0 )
+                for ( k = 0; k < s_pHMan->nWordsCur; k++ )
+                    puData[k] = ~puData0[k];
+            else
+                for ( k = 0; k < s_pHMan->nWordsCur; k++ )
+                    puData[k] = puData0[k];
+            continue;
+        }
+        // get the pointers to simulation data
+        puData  = Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+i-nLeaves);
+        puData0 = ((int)pHFan0->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan0->Num) : 
+                                                Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan0->Num-nLeaves);
+        puData1 = ((int)pHFan1->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan1->Num) : 
+                                                Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan1->Num-nLeaves);
+        // here are the phases
+        fComp0 = Abc_HObjFaninC0(pHObj) ^ (fUsePhase && (int)pHFan0->Num < nLeaves && pHFan0->fPhase);
+        fComp1 = Abc_HObjFaninC1(pHObj) ^ (fUsePhase && (int)pHFan1->Num < nLeaves && pHFan1->fPhase);
+        // simulate
+        if ( fComp0 && fComp1 )
+            for ( k = 0; k < s_pHMan->nWordsCur; k++ )
+                puData[k] = ~puData0[k] & ~puData1[k];
+        else if ( fComp0 )
+            for ( k = 0; k < s_pHMan->nWordsCur; k++ )
+                puData[k] = ~puData0[k] & puData1[k];
+        else if ( fComp1 )
+            for ( k = 0; k < s_pHMan->nWordsCur; k++ )
+                puData[k] = puData0[k] & ~puData1[k];
+        else 
+            for ( k = 0; k < s_pHMan->nWordsCur; k++ )
+                puData[k] = puData0[k] & puData1[k];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_HManSimulate( Vec_Ptr_t * vCone0, Vec_Ptr_t * vCone1, int nLeaves, int * pPhase )
+{
+    unsigned * pDataTop, * pDataLast;
+    int w;
+    // simulate the first one
+    Abc_HManSimulateOne( vCone0, nLeaves, 0 );
+    // save the last simulation value
+    pDataTop = Vec_PtrEntry( s_pHMan->vSims, ((Abc_HObj_t *)Vec_PtrEntryLast(vCone0))->Num );
+    pDataLast = Vec_PtrEntry( s_pHMan->vSims, Vec_PtrSize(s_pHMan->vSims)-1 );
+    for ( w = 0; w < s_pHMan->nWordsCur; w++ )
+        pDataLast[w] = pDataTop[w];
+    // simulate the other one
+    Abc_HManSimulateOne( vCone1, nLeaves, 1 );
+    // complement the output if needed
+    pDataTop = Vec_PtrEntry( s_pHMan->vSims, ((Abc_HObj_t *)Vec_PtrEntryLast(vCone1))->Num );
+    // mask unused bits
+    if ( nLeaves < 5 )
+    {
+        pDataTop[0]  &= ((~((unsigned)0)) >> (32-(1<<nLeaves)));
+        pDataLast[0] &= ((~((unsigned)0)) >> (32-(1<<nLeaves)));
+    }
+    if ( *pPhase = ((pDataTop[0] & 1) != (pDataLast[0] & 1)) )
+        for ( w = 0; w < s_pHMan->nWordsCur; w++ )
+            pDataTop[w] = ~pDataTop[w];
+    // compare
+    for ( w = 0; w < s_pHMan->nWordsCur; w++ )
+        if ( pDataLast[w] != pDataTop[w] )
+            return 0;
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 88188655..48b7eb92 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -73,7 +73,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
     int clkBdd, clkUnate;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
         return;
 clkBdd = clock() - clk;
 
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 5690013b..f1ec3847 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     }
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1 );    
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
@@ -331,7 +331,11 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
-    Abc_NtkBddToSop( pNtkNew, 0 );
+    if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
+    {
+        printf( "Converting to SOPs has failed.\n" );
+        return NULL;
+    }
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index c178c013..8d8784e0 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -713,7 +713,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
 Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj, *pObjNew;
+    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;//, *pObjNew;
     Abc_Obj_t * pMiter, * pTotal;
     Vec_Ptr_t * vCone;
     int i, k;
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
index c92667a3..77de5185 100644
--- a/src/base/abci/abcVanImp.c
+++ b/src/base/abci/abcVanImp.c
@@ -870,7 +870,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
 {
     Abc_Ntk_t * pNtkNew; 
     Vec_Ptr_t * vCone;
-    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew;
+    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;//, * pObjNew;
     unsigned Imp;
     int i, k;
 
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 5456693b..e0c65058 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -85,7 +85,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -112,6 +112,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
 ***********************************************************************/
 void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
 {
+    Prove_Params_t Params, * pParams = &Params;
 //    Fraig_Params_t Params;
 //    Fraig_Man_t * pMan;
     Abc_Ntk_t * pMiter;
@@ -171,7 +172,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Abc_NtkDelete( pMiter );
 */
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterProve( &pMiter, 0, 0, 1, 1, 0 );
+    Prove_ParamsSetDefault( pParams );
+    pParams->nItersMax = 5;
+    RetValue = Abc_NtkMiterProve( &pMiter, pParams );
     if ( RetValue == -1 )
         printf( "Networks are undecided (resource limits is reached).\n" );
     else if ( RetValue == 0 )
@@ -254,7 +257,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
diff --git a/src/base/abci/abc_.c b/src/base/abci/abc_.c
index 50558bdb..75ec88c3 100644
--- a/src/base/abci/abc_.c
+++ b/src/base/abci/abc_.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -40,6 +40,7 @@
 
 ***********************************************************************/
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 4339b520..41223c0b 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -10,6 +10,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFpga.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
+        src/base/abci/abcGen.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
@@ -22,11 +23,13 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcRestruct.c \
     src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \
+    src/base/abci/abcRr.c \
     src/base/abci/abcSat.c \
     src/base/abci/abcStrash.c \
     src/base/abci/abcSweep.c \
     src/base/abci/abcSymm.c \
     src/base/abci/abcTiming.c \
+    src/base/abci/abcTrace.c \
     src/base/abci/abcUnate.c \
     src/base/abci/abcUnreach.c \
     src/base/abci/abcVanEijk.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index c2c09697..0d90679d 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -18,6 +18,10 @@
 
 ***********************************************************************/
  
+#ifdef WIN32
+#include <process.h> 
+#endif
+
 #include "mainInt.h"
 #include "cmdInt.h"
 #include "abc.h"
@@ -45,6 +49,7 @@ static int CmdCommandLs            ( Abc_Frame_t * pAbc, int argc, char ** argv
 #endif
 static int CmdCommandSis           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandMvsis         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandCapo          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -85,6 +90,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "Various", "sis",     CmdCommandSis,            1); 
     Cmd_CommandAdd( pAbc, "Various", "mvsis",   CmdCommandMvsis,          1); 
+    Cmd_CommandAdd( pAbc, "Various", "capo",    CmdCommandCapo,           0); 
 }
 
 /**Function********************************************************************
@@ -1253,6 +1259,11 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    if ( pNetlist == NULL )
+    {
+        fprintf( pErr, "Cannot produce the intermediate network.\n" );
+        goto usage;
+    }
     Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
@@ -1389,6 +1400,11 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
 
     // write out the current network
     pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    if ( pNetlist == NULL )
+    {
+        fprintf( pErr, "Cannot produce the intermediate network.\n" );
+        goto usage;
+    }
     Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
@@ -1454,6 +1470,190 @@ usage:
 }
 
 
+/**Function********************************************************************
+
+  Synopsis    [Calls Capo internally.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNetlist;
+    char Command[1000], Buffer[100];
+    char * pProgNameCapoWin     = "capo.exe";
+    char * pProgNameCapoUnix    = "capo";
+    char * pProgNameGnuplotWin  = "wgnuplot.exe";
+    char * pProgNameGnuplotUnix = "gnuplot";
+    char * pProgNameCapo;
+    char * pProgNameGnuplot;
+    char * pPlotFileName;
+    int i;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        goto usage;
+    }
+
+    if ( strcmp( argv[0], "capo" ) != 0 )
+    {
+        fprintf( pErr, "Wrong command: \"%s\".\n", argv[0] );
+        goto usage;
+    }
+
+    if ( argc > 1 )
+    {
+        if ( strcmp( argv[1], "-h" ) == 0 )
+            goto usage;
+        if ( strcmp( argv[1], "-?" ) == 0 )
+            goto usage;
+    }
+
+    // get the names from the resource file
+    if ( Cmd_FlagReadByName(pAbc, "capowin") )
+        pProgNameCapoWin = Cmd_FlagReadByName(pAbc, "capowin");
+    if ( Cmd_FlagReadByName(pAbc, "capounix") )
+        pProgNameCapoUnix = Cmd_FlagReadByName(pAbc, "capounix");
+
+    // check if capo is available
+    if ( (pFile = fopen( pProgNameCapoWin, "r" )) )
+        pProgNameCapo = pProgNameCapoWin;
+    else if ( (pFile = fopen( pProgNameCapoUnix, "r" )) )
+        pProgNameCapo = pProgNameCapoUnix;
+    else if ( pFile == NULL )
+    {
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pProgNameCapoWin, pProgNameCapoUnix );
+        goto usage;
+    }
+    fclose( pFile );
+
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+    {
+        Abc_NtkUnmap(pNtk);
+        printf( "The current network is unmapped before calling Capo.\n" );
+    }
+
+    // write out the current network
+    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
+    if ( pNetlist == NULL )
+    {
+        fprintf( pErr, "Cannot produce the intermediate network.\n" );
+        goto usage;
+    }
+    Io_WriteBlif( pNetlist, "_capo_in.blif", 1 );
+    Abc_NtkDelete( pNetlist );
+
+    // create the file for Capo
+    sprintf( Command, "%s -f _capo_in.blif -log out.txt ", pProgNameCapo );
+    pPlotFileName = NULL;
+    for ( i = 1; i < argc; i++ )
+    {
+        sprintf( Buffer, " %s", argv[i] );
+        strcat( Command, Buffer );
+        if ( !strcmp( argv[i], "-plot" ) )
+            pPlotFileName = argv[i+1];
+    }
+
+    // call Capo
+    if ( system( Command ) )
+    {
+        fprintf( pErr, "The following command has returned non-zero exit status:\n" );
+        fprintf( pErr, "\"%s\"\n", Command );
+        unlink( "_capo_in.blif" );
+        goto usage;
+    }
+    // remove temporary networks
+    unlink( "_capo_in.blif" );
+    if ( pPlotFileName == NULL )
+        return 0;
+
+    // get the file name
+    sprintf( Buffer, "%s.plt", pPlotFileName );
+    pPlotFileName = Buffer;
+
+    // read in the Capo plotting output
+    if ( (pFile = fopen( pPlotFileName, "r" )) == NULL )
+    {
+        fprintf( pErr, "Cannot open the plot file \"%s\".\n\n", pPlotFileName );
+        goto usage;
+    }
+    fclose( pFile );
+
+    // get the names from the plotting software
+    if ( Cmd_FlagReadByName(pAbc, "gnuplotwin") )
+        pProgNameGnuplotWin = Cmd_FlagReadByName(pAbc, "gnuplotwin");
+    if ( Cmd_FlagReadByName(pAbc, "gnuplotunix") )
+        pProgNameGnuplotUnix = Cmd_FlagReadByName(pAbc, "gnuplotunix");
+
+    // check if Gnuplot is available
+    if ( (pFile = fopen( pProgNameGnuplotWin, "r" )) )
+        pProgNameGnuplot = pProgNameGnuplotWin;
+    else if ( (pFile = fopen( pProgNameGnuplotUnix, "r" )) )
+        pProgNameGnuplot = pProgNameGnuplotUnix;
+    else if ( pFile == NULL )
+    {
+        fprintf( pErr, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pProgNameGnuplotWin, pProgNameGnuplotUnix );
+        goto usage;
+    }
+    fclose( pFile );
+
+    // spawn the viewer
+#ifdef WIN32
+    if ( _spawnl( _P_NOWAIT, pProgNameGnuplot, pProgNameGnuplot, pPlotFileName, NULL ) == -1 )
+    {
+        fprintf( stdout, "Cannot find \"%s\".\n", pProgNameGnuplot );
+        goto usage;
+    }
+#else
+    {
+        sprintf( Command, "%s %s ", pProgNameGnuplot, pPlotFileName );
+        if ( system( Command ) == -1 )
+        {
+            fprintf( stdout, "Cannot execute \"%s\".\n", Command );
+            goto usage;
+        }
+    }
+#endif
+
+    // remove temporary networks
+//    unlink( pPlotFileName );
+    return 0;
+
+usage:
+    fprintf( pErr, "\n" );
+    fprintf( pErr, "Usage: capo [-h] <com>\n");
+    fprintf( pErr, "         peforms placement of the current network using Capo\n" );
+    fprintf( pErr, "         a Capo binary should be present in the same directory\n" );
+    fprintf( pErr, "         (if plotting, the Gnuplot binary should also be present)\n" );
+    fprintf( pErr, "   -h  : print the command usage\n" );
+    fprintf( pErr, " <com> : a Capo command\n" );
+    fprintf( pErr, "         Example 1: capo\n" );
+    fprintf( pErr, "                    (performs placement with default options)\n" );
+    fprintf( pErr, "         Example 2: capo -AR <aspec_ratio> -WS <whitespace_percentage> -save\n" );
+    fprintf( pErr, "                    (specifies the aspect ratio [default = 1.0] and\n" );
+    fprintf( pErr, "                    the whitespace percentage [0%%; 100%%) [default = 15%%])\n" );
+    fprintf( pErr, "         Example 3: capo -plot <base_fileName>\n" );
+    fprintf( pErr, "                    (produces <base_fileName.plt> and visualize it using Gnuplot)\n" );
+    fprintf( pErr, "         Example 4: capo -help\n" );
+    fprintf( pErr, "                    (prints the default usage message of the Capo binary)\n" );
+    fprintf( pErr, "         Please refer to the Capo webpage for additional information:\n" );
+    fprintf( pErr, "         http://vlsicad.eecs.umich.edu/BK/PDtools/\n" );
+    return 1;                    // error exit 
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 6422461c..70e648a7 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -42,6 +42,9 @@
 Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
 {
     Abc_Ntk_t * pNtk, * pTemp;
+//    extern int s_TotalNodes;
+//    extern int s_TotalChanges;
+//    s_TotalNodes = s_TotalChanges = 0;
     // set the new network
     if ( Extra_FileNameCheckExtension( pFileName, "blif" ) )
         pNtk = Io_ReadBlif( pFileName, fCheck );
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 1cb0ae5d..aa7f82e3 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -136,7 +136,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     Abc_ObjSetData( pNode, Abc_SopCreateNor(pNtk->pManFunc, nNames) );
                 else if ( strcmp(pType, "XOR") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateXor(pNtk->pManFunc, nNames) );
-                else if ( strcmp(pType, "NXOR") == 0 )
+                else if ( strcmp(pType, "NXOR") == 0 || strcmp(pType, "XNOR") == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateNxor(pNtk->pManFunc, nNames) );
                 else if ( strncmp(pType, "BUF", 3) == 0 )
                     Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) );
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 9e5ceb9f..24612566 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -23,6 +23,8 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
+ 
+static Abc_Ntk_t * s_pNtk = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -57,15 +59,51 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
         fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" );
         return 0;
     }
+    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" );
+        return 0;
+    }
     // create solver with clauses
-    pSat = Abc_NtkMiterSatCreate( pNtk );
+    pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
+    if ( pSat == NULL )
+    {
+        fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
+        return 1;
+    }        
     // write the clauses
+    s_pNtk = pNtk;
     Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
+    s_pNtk = NULL;
     // free the solver
     solver_delete( pSat );
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Output the mapping of PIs into variable numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars )
+{
+    extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+    Abc_Ntk_t * pNtk = s_pNtk;
+    Vec_Int_t * vCiIds;
+    Abc_Obj_t * pObj;
+    int i;
+    vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
+    fprintf( pFile, "c PI variable numbers: <PI_name> <SAT_var_number>\n" );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        fprintf( pFile, "c %s %d\n", Abc_ObjName(pObj), Vec_IntEntry(vCiIds, i) + (int)(incrementVars > 0) );
+    Vec_IntFree( vCiIds );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index dbf157bf..ed6acb24 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -412,7 +412,13 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return;
+        }
+    }
 
     // mark the nodes from the set
     Vec_PtrForEachEntry( vNodes, pNode, i )
diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c
index ab216eb3..f0981a8e 100644
--- a/src/base/io/ioWriteList.c
+++ b/src/base/io/ioWriteList.c
@@ -120,8 +120,8 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost )
     if ( Abc_ObjFanoutNum( Abc_NtkConst1(pNtk) ) > 0 )
         Io_WriteListEdge( pFile, Abc_NtkConst1(pNtk) );
 
-    // write the PO edges
-    Abc_NtkForEachCi( pNtk, pObj, i )
+    // write the PI edges
+    Abc_NtkForEachPi( pNtk, pObj, i )
         Io_WriteListEdge( pFile, pObj );
 
     // write the internal nodes
@@ -132,7 +132,7 @@ void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int fUseHost )
     if ( fUseHost )
         Io_WriteListHost( pFile, pNtk );
     else
-        Abc_NtkForEachCo( pNtk, pObj, i )
+        Abc_NtkForEachPo( pNtk, pObj, i )
             Io_WriteListEdge( pFile, pObj );
 
     fprintf( pFile, "\n" );
@@ -157,12 +157,13 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj )
     fprintf( pFile, "%-10s >    ", Abc_ObjName(pObj) );
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
-        fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pFanout), Abc_ObjName(pObj), Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
-        if ( i == Abc_ObjFanoutNum(pObj) - 1 )
-            fprintf( pFile, "." );
-        else
+        fprintf( pFile, " %s", Abc_ObjName(pFanout) );
+        fprintf( pFile, " ([%s_to_", Abc_ObjName(pObj) );
+        fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) );
+        if ( i != Abc_ObjFanoutNum(pObj) - 1 )
             fprintf( pFile, "," );
     }
+    fprintf( pFile, "." );
     fprintf( pFile, "\n" );
 }
 
@@ -186,22 +187,19 @@ void Io_WriteListHost( FILE * pFile, Abc_Ntk_t * pNtk )
     {
         fprintf( pFile, "%-10s >    ", Abc_ObjName(pObj) );
         fprintf( pFile, " %s ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), "HOST", 0 );
-        if ( i == Abc_NtkPoNum(pNtk) - 1 )
-            fprintf( pFile, "." );
-        else
-            fprintf( pFile, "," );
+        fprintf( pFile, "." );
+        fprintf( pFile, "\n" );
     }
-    fprintf( pFile, "\n" );
 
     fprintf( pFile, "%-10s >    ", "HOST" );
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
-        fprintf( pFile, " %s ([%s_to_%s] = %d)", Abc_ObjName(pObj), "HOST", Abc_ObjName(pObj), 0 );
-        if ( i == Abc_NtkPiNum(pNtk) - 1 )
-            fprintf( pFile, "." );
-        else
+        fprintf( pFile, " %s", Abc_ObjName(pObj) );
+        fprintf( pFile, " ([%s_to_%s] = %d)", "HOST", Abc_ObjName(pObj), 0 );
+        if ( i != Abc_NtkPiNum(pNtk) - 1 )
             fprintf( pFile, "," );
     }
+    fprintf( pFile, "." );
     fprintf( pFile, "\n" );
 }
 
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 9b483904..fe511314 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -81,6 +81,7 @@ extern FILE *          Abc_FrameReadErr( Abc_Frame_t * p );
 extern bool            Abc_FrameReadMode( Abc_Frame_t * p );
 extern bool            Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
 extern void            Abc_FrameRestart( Abc_Frame_t * p );
+extern bool            Abc_FrameShowProgress( Abc_Frame_t * p );
 
 extern void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index b3208740..5747443c 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -111,9 +111,12 @@ Abc_Frame_t * Abc_FrameAllocate()
     // set the starting step
     p->nSteps = 1;
     p->fBatchMode = 0;
+    p->fProgress = 1;
     // initialize decomposition manager
     define_cube_size(20);
     set_espresso_flags();
+    // initialize the trace manager
+//    Abc_HManStart();
     return p;
 }
 
@@ -132,6 +135,7 @@ Abc_Frame_t * Abc_FrameAllocate()
 void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void undefine_cube_size();
+//    Abc_HManStop();
     undefine_cube_size();
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
@@ -155,6 +159,22 @@ void Abc_FrameRestart( Abc_Frame_t * p )
 {
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FrameShowProgress( Abc_Frame_t * p )
+{
+    return p->fProgress;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index d2bca1ab..109e91c8 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -55,6 +55,7 @@ struct Abc_Frame_t_
     int             nSteps;      // the counter of different network processed
     int             fAutoexac;   // marks the autoexec mode
     int                fBatchMode;     // are we invoked in batch mode?
+    int             fProgress;   // shows progress bars
     // output streams
     FILE *          Out;
     FILE *          Err;
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index e74f3fa7..813b1ed8 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -358,7 +358,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     // solve the miter
 clk = clock();
 //    RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 );
-    RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0 );
+    RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0, 0 );
 if ( fVerbose )
 if ( clock() - clk > 100 )
 {
diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c
index 67ac4a7d..185c05f3 100644
--- a/src/base/seq/seqMapIter.c
+++ b/src/base/seq/seqMapIter.c
@@ -613,7 +613,7 @@ void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk )
         if ( pList == NULL )
             continue;
         for ( pCut = pList->pNext; pCut; pCut = pCut->pNext )
-            Cut_TruthCanonicize( pCut );
+            Cut_TruthNCanonicize( pCut );
     }
 }
 
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 0805a838..38915bf4 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -107,7 +107,13 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk, 0);
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
 
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );