Version abc90313

21 files changed, 1196 insertions, 229 deletions

diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 96bddbcb..f3d3dea9 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -129,6 +129,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
     double clkTotal = clock();
     // sweep for equivalences
     Cec_ManFraSetDefaultParams( pParsFra );
+    pParsFra->nItersMax    = 1000;
     pParsFra->nBTLimit     = pPars->nBTLimit;
     pParsFra->TimeLimit    = pPars->TimeLimit;
     pParsFra->fVerbose     = pPars->fVerbose;
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 0cac88af..26ff543a 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -242,6 +242,7 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
         }
         else
         {
+            assert( Repr < Ent );
             Gia_ObjSetRepr( p, Ent, Repr );
             Gia_ObjSetNext( p, EntPrev, Ent );
             EntPrev = Ent;
@@ -500,7 +501,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
 
 ***********************************************************************/
 void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
-{
+{ 
     unsigned * pInfo;
     int i, ScoreBest = 0, iPatBest = 1;
     // find the best pattern
@@ -838,7 +839,7 @@ int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
     p->nWords = p->pPars->nWords;
     for ( i = 0; i < p->pPars->nRounds; i++ )
     {
-        if ( (i % 4) == 0 && p->pPars->fVerbose )
+        if ( (i % (p->pPars->nRounds / 5)) == 0 && p->pPars->fVerbose )
             Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
         Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
         if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 061c3a7d..8e66179f 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -90,10 +90,10 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
 void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSmf_t) );
-    p->nWords         =      15;  // the number of simulation words
-    p->nRounds        =      15;  // the number of simulation rounds
+    p->nWords         =      31;  // the number of simulation words
+    p->nRounds        =       1;  // the number of simulation rounds
     p->nFrames        =       2;  // the number of time frames
-    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->nBTLimit       =     100;  // conflict limit at a node
     p->TimeLimit      =       0;  // the runtime limit in seconds
     p->fDualOut       =       0;  // miter with separate outputs
     p->fCheckMiter    =       0;  // the circuit is the miter
@@ -118,8 +118,8 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
     p->nWords         =      15;  // the number of simulation words
     p->nRounds        =      15;  // the number of simulation rounds
     p->TimeLimit      =       0;  // the runtime limit in seconds
-    p->nItersMax      =    1000;  // the maximum number of iterations of SAT sweeping
-    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->nItersMax      =      10;  // the maximum number of iterations of SAT sweeping
+    p->nBTLimit       =     100;  // conflict limit at a node
     p->nLevelMax      =       0;  // restriction on the level of nodes to be swept
     p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
     p->fRewriting     =       0;  // enables AIG rewriting
@@ -322,6 +322,8 @@ p->timeSat += clock() - clk;
         // update the manager
         pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
         Gia_ManStop( pTemp );
+        if ( p->pAig == NULL )
+            break;
         if ( p->pPars->fVerbose )
         {
             printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", 
@@ -381,7 +383,7 @@ finalize:
     }
 
     pTemp = p->pAig; p->pAig = NULL;
-    if ( pTemp == NULL )
+    if ( pTemp == NULL && pSim->iOut >= 0 )
         printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
     else if ( pSim->pCexes )
         printf( "Disproved %d outputs of the miter.\n", pSim->nOuts );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 6cb229ae..1a398e2e 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -255,7 +255,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
     Gia_Man_t * pSrm;
     int r, nPats, RetValue = -1;
     if ( pAig->pReprs == NULL )
-    {
+    { 
         printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
         return -1;
     }
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 2b6997e1..24d5c3ed 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -703,7 +703,8 @@ void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pP
     }
     p->timeTotal = clock() - clk;
     Bar_ProgressStop( pProgress );
-//    Cec_ManSatPrintStats( p );
+    if ( pPars->fVerbose )
+        Cec_ManSatPrintStats( p );
     Cec_ManSatStop( p );
     if ( pnPats )
         *pnPats = iPat-1;
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c5d55565..1c3529ba 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -67,6 +67,11 @@ struct Gia_Obj_t_
 
     unsigned       Value;         // application-specific value
 };
+// Value is currently use to store several types of information
+// - pointer to the next node in the hash table during structural hashing
+// - pointer to the node copy during duplication 
+// - traversal ID of the node during traversal
+// - reference counter of the node (will not be used in the future)
 
 // sequential counter-example
 typedef struct Gia_Cex_t_   Gia_Cex_t;
@@ -177,6 +182,7 @@ static inline int          Gia_ManPoNum( Gia_Man_t * p )       { return Vec_IntS
 static inline int          Gia_ManRegNum( Gia_Man_t * p )      { return p->nRegs;              }
 static inline int          Gia_ManObjNum( Gia_Man_t * p )      { return p->nObjs;              }
 static inline int          Gia_ManAndNum( Gia_Man_t * p )      { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1;  }
+static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                          }
 
 static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                               }
 static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                              }
@@ -193,6 +199,7 @@ static inline int          Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj )            {
 static inline int          Gia_ObjIsCi( Gia_Obj_t * pObj )                     { return pObj->fTerm && pObj->iDiff0 == GIA_NONE; } 
 static inline int          Gia_ObjIsCo( Gia_Obj_t * pObj )                     { return pObj->fTerm && pObj->iDiff0 != GIA_NONE; } 
 static inline int          Gia_ObjIsAnd( Gia_Obj_t * pObj )                    { return!pObj->fTerm && pObj->iDiff0 != GIA_NONE; } 
+static inline int          Gia_ObjIsCand( Gia_Obj_t * pObj )                   { return Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj); } 
 static inline int          Gia_ObjIsConst0( Gia_Obj_t * pObj )                 { return pObj->iDiff0 == GIA_NONE && pObj->iDiff1 == GIA_NONE; } 
 static inline int          Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ return pObj == p->pObjs;                        } 
 
@@ -232,6 +239,12 @@ static inline int          Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFani
 static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );     }
 static inline int          Gia_ObjFanin1Copy( Gia_Obj_t * pObj )               { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );     }
 
+static inline int          Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)];  }
+static inline void         Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit;  }
+
+static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
+static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
+
 static inline Gia_Obj_t *  Gia_ObjFromLit( Gia_Man_t * p, int iLit )           { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) );  }
 static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_Var2Lit( Gia_ObjId(p, pObj), Gia_IsComplement(pObj) );              }
 static inline int          Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit )      { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) );        }
@@ -397,6 +410,8 @@ static inline int *      Gia_ObjGateFanins( Gia_Man_t * p, int Id )         { re
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
 #define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i )             \
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
+#define Gia_ManForEachObjReverse( p, pObj, i )                          \
+    for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
 #define Gia_ManForEachAnd( p, pObj, i )                                 \
     for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )  if ( !Gia_ObjIsAnd(pObj) ) {} else
 #define Gia_ManForEachCi( p, pObj, i )                                  \
@@ -429,6 +444,9 @@ extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
 /*=== giaCof.c ============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
+extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
+extern Gia_Man_t *         Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose );
+extern Gia_Man_t *         Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose );
 /*=== giaDfs.c ============================================================*/
 extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
 extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes );
@@ -436,6 +454,7 @@ extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNo
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
 /*=== giaDup.c ============================================================*/
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
+extern Gia_Man_t *         Gia_ManDupSelf( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
@@ -444,22 +463,23 @@ extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupNormalized( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos );
-extern Gia_Man_t *         Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nLimFan );
 extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose );
 extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 /*=== giaEnable.c ==========================================================*/
-extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset );
+extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
+extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
 /*=== giaEquiv.c ==========================================================*/
+extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
 extern void                Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
 extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
-extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll );
+extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
 extern Gia_Man_t *         Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
 extern int                 Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
-extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut );
+extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
 /*=== giaFanout.c =========================================================*/
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 544cfe0d..3f707e1c 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -205,6 +205,29 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
+{
+    Aig_Man_t * pMan;
+    Gia_Man_t * pGia, * pTemp;
+    pGia = Gia_ManFromAig( p );
+    pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
+    Gia_ManStop( pTemp );
+    pMan = Gia_ManToAig( pGia );
+    Gia_ManStop( pGia );
+    return pMan;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index cfd2dc73..da1a8c9f 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -230,6 +230,7 @@ Gia_Rpr_t * Gia_ReadEquivClasses( unsigned char ** ppPos, int nSize )
         iNode += Item;
         pReprs[iNode].fProved = fProved;
         pReprs[iNode].iRepr = iRepr;
+        assert( iRepr < iNode );
 //printf( "Node = %d ", iNode );
     }
     return pReprs;
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index 735aca72..c5efa839 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -685,6 +685,232 @@ ABC_PRT( "Time", clock() - clk );
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj, * pPivot;
+    int i, iCofVar = -1;
+    if ( !(iVar > 0 && iVar < Gia_ManObjNum(p)) )
+    {
+        printf( "Gia_ManDupCof(): Variable %d is out of range (%d; %d).\n", iVar, 0, Gia_ManObjNum(p) );
+        return NULL;
+    }
+    // find the cofactoring variable
+    pPivot = Gia_ManObj( p, iVar );
+    if ( !Gia_ObjIsCand(pPivot) )
+    {
+        printf( "Gia_ManDupCof(): Variable %d should be a CI or an AND node.\n", iVar );
+        return NULL;
+    }
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    // compute negative cofactor
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        pObj->Value = Gia_ManAppendCi(pNew);
+        if ( pObj == pPivot )
+        {
+            iCofVar = pObj->Value;
+            pObj->Value = Gia_Var2Lit( 0, 0 );
+        }
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( pObj == pPivot )
+        {
+            iCofVar = pObj->Value;
+            pObj->Value = Gia_Var2Lit( 0, 0 );
+        }
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    // compute the positive cofactor
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
+        if ( pObj == pPivot )
+            pObj->Value = Gia_Var2Lit( 0, 1 );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( pObj == pPivot )
+            pObj->Value = Gia_Var2Lit( 0, 1 );
+    }
+    // create MUXes
+    assert( iCofVar > 0 );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        if ( pObj->Value == (unsigned)Gia_ObjFanin0Copy(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        else
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashMux(pNew, iCofVar, Gia_ObjFanin0Copy(pObj), pObj->Value) );
+    }
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar )
+{
+    Gia_Man_t * pNew, * pTemp;
+    pNew = Gia_ManDupCofInt( p, iVar );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Determines variables whose fanout count is higher than this.]
+
+  Description [Variables are returned in a reverse topological order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManCofVars( Gia_Man_t * p, int nFanLim )
+{
+    Vec_Int_t * vVars;
+    Gia_Obj_t * pObj;
+    int i;
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    vVars = Vec_IntAlloc( 100 );
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjIsCand(pObj) && Gia_ObjRefs(p, pObj) >= nFanLim )
+            Vec_IntPush( vVars, i );
+    ABC_FREE( p->pRefs );
+    return vVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers attributes from the original one to the final one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManTransfer( Gia_Man_t * pAig, Gia_Man_t * pCof, Gia_Man_t * pNew, Vec_Int_t * vSigs )
+{
+    Vec_Int_t * vSigsNew;
+    Gia_Obj_t * pObj, * pObjF;
+    int i;
+    vSigsNew = Vec_IntAlloc( 100 );
+    Gia_ManForEachObjVec( vSigs, pAig, pObj, i )
+    {
+        assert( Gia_ObjIsCand(pObj) );
+        pObjF = Gia_ManObj( pCof, Gia_Lit2Var(pObj->Value) );
+        if ( pObjF->Value && ~pObjF->Value )
+            Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) );
+    }
+    return vSigsNew;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cofactors selected variables (should be in reverse topo order).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose )
+{
+    Vec_Int_t * vSigsNew, * vTemp;
+    Gia_Man_t * pAig, * pCof, * pNew;
+    int iVar;
+    if ( fVerbose )
+    { 
+        printf( "Cofactoring %d signals.\n", Vec_IntSize(vSigs) );
+        Gia_ManPrintStats( p );
+    }
+    if ( Vec_IntSize( vSigs ) > 200 )
+    {
+        printf( "Too many signals to cofactor.\n" );
+        return NULL;
+    }
+    pAig = Gia_ManDup( p );
+    vSigsNew = Vec_IntDup( vSigs );
+    while ( Vec_IntSize(vSigsNew) > 0 )
+    {
+        Vec_IntSort( vSigsNew, 0 );
+        iVar = Vec_IntPop( vSigsNew );
+//        Gia_ManCreateRefs( pAig );
+//        printf( "ref count = %d\n", Gia_ObjRefs( pAig, Gia_ManObj(pAig, iVar) ) );
+//        ABC_FREE( pAig->pRefs );
+        pCof = Gia_ManDupCofInt( pAig, iVar );
+        pNew = Gia_ManCleanup( pCof );
+        vSigsNew = Gia_ManTransfer( pAig, pCof, pNew, vTemp = vSigsNew );
+        Vec_IntFree( vTemp );
+        Gia_ManStop( pAig );
+        Gia_ManStop( pCof );
+        pAig = pNew;
+        if ( fVerbose )
+            printf( "Cofactored variable %d.\n", iVar );
+        if ( fVerbose )
+            Gia_ManPrintStats( pAig );
+    }
+    Vec_IntFree( vSigsNew );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cofactors all variables whose fanout is higher than this.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vSigs = Gia_ManCofVars( p, nFanLim );
+    pNew = Gia_ManDupCofAllInt( p, vSigs, fVerbose );
+    Vec_IntFree( vSigs );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 1d940b78..5fb801a7 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -62,6 +62,45 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates while adding self-loops to the registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp; 
+    Gia_Obj_t * pObj;
+    int i, iCtrl;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    iCtrl = Gia_ManAppendCi( pNew );
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ManHashMux( pNew, iCtrl, Gia_ObjFanin0Copy(pObj), Gia_ObjRiToRo(p, pObj)->Value );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, pObj->Value );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG without any changes.]
 
   Description []
@@ -192,22 +231,22 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( ~pObj->Value )
         return pObj->Value;
     if ( p->pReprsOld && ~p->pReprsOld[Gia_ObjId(p, pObj)] )
     {
         Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] );
-        pRepr->Value = Gia_ManDupDfs_rec( pNew, p, pRepr );
+        pRepr->Value = Gia_ManDupDfs2_rec( pNew, p, pRepr );
         return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     }
     if ( Gia_ObjIsCi(pObj) )
         return pObj->Value = Gia_ManAppendCi(pNew);
-    Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin0(pObj) );
     if ( Gia_ObjIsCo(pObj) )
         return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin1(pObj) );
     if ( pNew->pHTable )
         return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -224,7 +263,7 @@ int Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
+Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pObjNew;
@@ -234,7 +273,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManDupDfs_rec( pNew, p, pObj );
+        Gia_ManDupDfs2_rec( pNew, p, pObj );
     Gia_ManForEachCi( p, pObj, i )
         if ( ~pObj->Value == 0 )
             pObj->Value = Gia_ManAppendCi(pNew);
@@ -253,6 +292,57 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupDfs_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
 
   Description []
@@ -332,7 +422,7 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
         pObj->Value = Gia_ManAppendCi(pNew);
     Vec_IntForEachEntry( vLits, iLit, i )
     {
-        iLitRes = Gia_ManDupDfs_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
+        iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
         Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
     }
     Gia_ManSetRegNum( pNew, 0 );
@@ -404,95 +494,6 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar, int nLimFan )
-{
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj, * pPivot;
-    int i, iCofVar = -1;
-    if ( nLimFan > 0 )
-    {
-        printf( "This feature is not implemented.\n" );
-        return NULL;
-    }
-    if ( !(iVar > 0 && iVar < Gia_ManObjNum(p)) )
-    {
-        printf( "Gia_ManDupCofactored(): Variable %d is out of range (%d; %d).\n", iVar, 0, Gia_ManObjNum(p) );
-        return NULL;
-    }
-    // find the cofactoring variable
-    pPivot = Gia_ManObj( p, iVar );
-    if ( !(Gia_ObjIsCi(pPivot) || Gia_ObjIsAnd(pPivot)) )
-    {
-        printf( "Gia_ManDupCofactored(): Variable %d should be a CI or an AND node.\n", iVar );
-        return NULL;
-    }
-//    assert( Gia_ManRegNum(p) == 0 );
-    pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    Gia_ManHashAlloc( pNew );
-    Gia_ManConst0(p)->Value = 0;
-    // compute negative cofactor
-    Gia_ManForEachCi( p, pObj, i )
-    {
-        pObj->Value = Gia_ManAppendCi(pNew);
-        if ( pObj == pPivot )
-        {
-            iCofVar = pObj->Value;
-            pObj->Value = Gia_Var2Lit( 0, 0 );
-        }
-    }
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        if ( pObj == pPivot )
-        {
-            iCofVar = pObj->Value;
-            pObj->Value = Gia_Var2Lit( 0, 0 );
-        }
-    }
-    Gia_ManForEachCo( p, pObj, i )
-        pObj->Value = Gia_ObjFanin0Copy(pObj);
-    // compute the positive cofactor
-    Gia_ManForEachCi( p, pObj, i )
-    {
-        pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
-        if ( pObj == pPivot )
-            pObj->Value = Gia_Var2Lit( 0, 1 );
-    }
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        if ( pObj == pPivot )
-            pObj->Value = Gia_Var2Lit( 0, 1 );
-    }
-    // create MUXes
-    assert( iCofVar > 0 );
-    Gia_ManForEachCo( p, pObj, i )
-    {
-        if ( pObj->Value == (unsigned)Gia_ObjFanin0Copy(pObj) )
-            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-        else
-            pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashMux(pNew, iCofVar, Gia_ObjFanin0Copy(pObj), pObj->Value) );
-    }
-    Gia_ManHashStop( pNew );
-    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
-    // rehash the result
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Print representatives.]
 
   Description []
@@ -544,7 +545,7 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
         int iLit, iLitRes;
         Vec_IntForEachEntry( vLits, iLit, i )
         {
-            iLitRes = Gia_ManDupDfs_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
+            iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
             Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
         }
     }
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index d05dc5a9..f80bc885 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -104,7 +104,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr )
     printf( "%s (total = %d  driven = %d)\n", pStr, Counter, nTotal );
     Counter = 0;
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
-        if ( pFreq[i] > 1 )
+        if ( pFreq[i] > 10 )
         {
             printf( "%3d :   Obj = %6d   Refs = %6d   Freq = %6d\n", 
                 ++Counter, i, Gia_ObjRefs(p, Gia_ManObj(p,i)), pFreq[i] );
@@ -124,7 +124,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset )
+void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose )
 {
     Vec_Int_t * vSuper;
     Gia_Obj_t * pFlop, * pObjC, * pObj0, * pObj1, * pNode, * pTemp;
@@ -189,20 +189,235 @@ void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset )
             }
     }
     Vec_IntFree( vSuper );
+    ABC_FREE( p->pRefs );
     Gia_ManCreateRefs( p );
-    printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable );
-    if ( fSetReset )
+    if ( fVerbose )
     {
-        Gia_ManPrintSignals( p, pSets, "Set signals" );
-        Gia_ManPrintSignals( p, pResets, "Reset signals" );
+        printf( "Flops with set/reset = %6d. Flops with enable = %6d.\n", nHaveSetReset, nHaveEnable );
+        if ( fSetReset )
+        {
+            Gia_ManPrintSignals( p, pSets, "Set signals" );
+            Gia_ManPrintSignals( p, pResets, "Reset signals" );
+        }
+        Gia_ManPrintSignals( p, pEnables, "Enable signals" );
     }
-    Gia_ManPrintSignals( p, pEnables, "Enable signals" );
     ABC_FREE( p->pRefs );
     ABC_FREE( pSets );
     ABC_FREE( pResets );
     ABC_FREE( pEnables );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManDetectSeqSignalsWithFanout( Gia_Man_t * p, int nFanMax, int fVerbose )
+{
+    Vec_Int_t * vResult;
+    Vec_Int_t * vSuper;
+    Gia_Obj_t * pFlop, * pObjC, * pObj0, * pObj1, * pNode, * pTemp;
+    int i, k, Ent, * pSets, * pResets, * pEnables;
+    int nHaveSetReset = 0, nHaveEnable = 0;
+    assert( Gia_ManRegNum(p) > 0 );
+    pSets    = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    pResets  = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    pEnables = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    vSuper   = Vec_IntAlloc( 100 );
+    Gia_ManForEachRi( p, pFlop, i )
+    {
+        pNode = Gia_ObjFanin0(pFlop);
+        if ( !Gia_ObjIsAnd(pNode) )
+            continue;
+        // detect sets/resets
+        Gia_CollectSuper( p, pNode, vSuper );
+        if ( Gia_ObjFaninC0(pFlop) )
+            Vec_IntForEachEntry( vSuper, Ent, k )
+                pSets[Ent]++;
+        else
+            Vec_IntForEachEntry( vSuper, Ent, k )
+                pResets[Ent]++;
+        // detect enables
+        if ( !Gia_ObjIsMuxType(pNode) )
+            continue;
+        pObjC = Gia_ObjRecognizeMux( pNode, &pObj0, &pObj1 );
+        pTemp = Gia_ObjRiToRo( p, pFlop );
+        if ( Gia_Regular(pObj0) != pTemp && Gia_Regular(pObj1) != pTemp )
+            continue;
+        if ( !Gia_ObjFaninC0(pFlop) )
+        {
+            pObj0 = Gia_Not(pObj0);
+            pObj1 = Gia_Not(pObj1);
+        }
+        if ( Gia_IsComplement(pObjC) )
+        {
+            pObjC = Gia_Not(pObjC);
+            pTemp = pObj0;
+            pObj0 = pObj1;
+            pObj1 = pTemp;
+        }
+        // detect controls
+//        Gia_CollectSuper( p, pObjC, vSuper );
+//        Vec_IntForEachEntry( vSuper, Ent, k )
+//            pEnables[Ent]++;
+        pEnables[Gia_ObjId(p, pObjC)]++;
+        nHaveEnable++;
+    }
+    Gia_ManForEachRi( p, pFlop, i )
+    {
+        pNode = Gia_ObjFanin0(pFlop);
+        if ( !Gia_ObjIsAnd(pNode) )
+            continue;
+        // detect sets/resets
+        Gia_CollectSuper( p, pNode, vSuper );
+        Vec_IntForEachEntry( vSuper, Ent, k )
+            if ( pSets[Ent] > 1 || pResets[Ent] > 1 )
+            {
+                nHaveSetReset++;
+                break;
+            }
+    }
+    Vec_IntFree( vSuper );
+    vResult  = Vec_IntAlloc( 100 );
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+        if ( pSets[i] > nFanMax )
+        {
+            if ( fVerbose )
+                printf( "Adding set signal %d related to %d flops.\n", i, pSets[i] );
+            Vec_IntPushUnique( vResult, i );
+        }
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+        if ( pResets[i] > nFanMax )
+        {
+            if ( fVerbose )
+                printf( "Adding reset signal %d related to %d flops.\n", i, pResets[i] );
+            Vec_IntPushUnique( vResult, i );
+        }
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+        if ( pEnables[i] > nFanMax )
+        {
+            if ( fVerbose )
+                printf( "Adding enable signal %d related to %d flops.\n", i, pEnables[i] );
+            Vec_IntPushUnique( vResult, i );
+        }
+    ABC_FREE( pSets );
+    ABC_FREE( pResets );
+    ABC_FREE( pEnables );
+    return vResult;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers attributes from the original one to the final one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManTransferFrames( Gia_Man_t * pAig, Gia_Man_t * pFrames, int nFrames, Gia_Man_t * pNew, Vec_Int_t * vSigs )
+{
+    Vec_Int_t * vSigsNew;
+    Gia_Obj_t * pObj, * pObjF;
+    int k, f;
+    vSigsNew = Vec_IntAlloc( 100 );
+    Gia_ManForEachObjVec( vSigs, pAig, pObj, k )
+    {
+        assert( Gia_ObjIsCand(pObj) );
+        for ( f = 0; f < nFrames; f++ )
+        {
+            pObjF = Gia_ManObj( pFrames, Gia_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) );
+            if ( pObjF->Value && ~pObjF->Value )
+                Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) );
+        }
+    }
+    return vSigsNew;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int f, i;
+    ABC_FREE( p->pCopies );
+    p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
+    pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ObjSetCopyF( p, 0, pObj, 0 );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+        Gia_ManForEachAnd( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) );
+        Gia_ManForEachCo( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
+        Gia_ManForEachPo( p, pObj, i )
+            Gia_ManAppendCo( pNew, Gia_ObjCopyF(p, f, pObj) );
+        if ( f == nFrames - 1 )
+            break;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) );
+    }
+    Gia_ManHashStop( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unrolls initialized timeframes while cofactoring some vars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose )
+{
+    Vec_Int_t * vCofSigs, * vTemp;
+    Gia_Man_t * pAig, * pFrames, * pNew;
+    // compute initialized timeframes
+    pFrames  = Gia_ManUnrollInit( p, nFrames );
+    pAig     = Gia_ManCleanup( pFrames );
+    // compute and remap set/reset/enable signals
+    vCofSigs = Gia_ManDetectSeqSignalsWithFanout( p, nFanMax, fVerbose );
+    vCofSigs = Gia_ManTransferFrames( p, pFrames, nFrames, pAig, vTemp = vCofSigs );
+    Vec_IntFree( vTemp );
+    Gia_ManStop( pFrames );
+    ABC_FREE( p->pCopies );
+    // cofactor all these variables
+    pNew = Gia_ManDupCofAllInt( pAig, vCofSigs, fVerbose );
+    Vec_IntFree( vCofSigs );
+    Gia_ManStop( pAig );
+    return pNew;
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index acdd3c13..b87c77e5 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -30,6 +30,57 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if AIG is not in the required topo order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr;
+    if ( pObj->Value == 0 )
+        return 1;
+    pObj->Value = 0;
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) ) )
+        return 0;
+    if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
+        return 0;
+    pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+    return pRepr == NULL || pRepr->Value == 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if AIG is not in the required topo order.]
+
+  Description [AIG should be in such an order that the representative
+  is always traversed before the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckTopoOrder( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, RetValue = 1;
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        RetValue &= Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin0(pObj) );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Given representatives, derives pointers to the next objects.]
 
   Description []
@@ -192,18 +243,21 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
+static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
 {
     if ( fUseAll )
     {
         if ( Gia_ObjRepr(p, Gia_ObjId(p,pObj)) == GIA_VOID )
             return NULL;
-    }
+    } 
     else
     {
         if ( !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
             return NULL;
     }
+//    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
+    if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjRepr(p, Gia_ObjId(p,pObj)) ) )
+        return NULL;
     return Gia_ManObj( p, Gia_ObjRepr(p, Gia_ObjId(p,pObj)) );
 }
 
@@ -218,20 +272,20 @@ static inline Gia_Obj_t * Gia_ManEquivRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll )
+void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int fUseAll, int fDualOut )
 {
     Gia_Obj_t * pRepr;
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
+    if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
     {
-        Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll );
+        Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
         pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
-    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
-    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll );
+    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
+    Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin1(pObj), fUseAll, fDualOut );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 }
 
@@ -246,12 +300,24 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
+Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pRepr;
     int i;
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    {
+        printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
+        return NULL;
+    }
+    if ( !Gia_ManCheckTopoOrder( p ) )
+    {
+        printf( "Gia_ManEquivReduce(): AIG is not in a correct topological order.\n" );
+        return NULL;
+    }
     Gia_ManSetPhase( p );
+    if ( fDualOut )
+        Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
@@ -259,12 +325,12 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll )
     Gia_ManForEachCi( p, pObj, i )
     {
         pObj->Value = Gia_ManAppendCi(pNew);
-        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll)) )
+        if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
             pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     }
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll );
+        Gia_ManEquivReduce_rec( pNew, p, Gia_ObjFanin0(pObj), fUseAll, fDualOut );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManHashStop( pNew );
@@ -386,6 +452,52 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
 
 /**Function*************************************************************
 
+  Synopsis    [Removes pointers to the unmarked nodes..]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vClass;
+    int i, k, iNode, iRepr, iPrev;
+    pNew = Gia_ManDupDfs( p );
+    // start representatives
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) );
+    for ( i = 0; i < Gia_ManObjNum(pNew); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    // iterate over constant candidates
+    Gia_ManForEachConst( p, i )
+        Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+    // iterate over class candidates
+    vClass = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, i )
+    {
+        Vec_IntClear( vClass );
+        Gia_ClassForEachObj( p, i, k )
+            Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
+        assert( Vec_IntSize( vClass ) > 1 );
+        Vec_IntSort( vClass, 0 );
+        iRepr = iPrev = Vec_IntEntry( vClass, 0 );
+        Vec_IntForEachEntryStart( vClass, iNode, k, 1 )
+        {
+            Gia_ObjSetRepr( pNew, iNode, iRepr );
+            assert( iPrev < iNode );
+            iPrev = iNode;
+        }
+    }
+    Vec_IntFree( vClass );
+    pNew->pNexts = Gia_ManDeriveNexts( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reduces AIG while remapping equivalence classes.]
 
   Description [Drops the pairs of outputs if they are proved equivalent.]
@@ -398,7 +510,9 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
 Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs )
 {
     Gia_Man_t * pNew, * pFinal;
-    pNew = Gia_ManEquivReduce( p, 0 );
+    pNew = Gia_ManEquivReduce( p, 0, 0, 0 );
+    if ( pNew == NULL )
+        return NULL;
     if ( fMiterPairs )
         Gia_ManEquivFixOutputPairs( pNew );
     if ( fSeq )
@@ -409,6 +523,8 @@ Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs
     pFinal = Gia_ManDupMarked( pNew );
     Gia_ManEquivDeriveReprs( p, pNew, pFinal );
     Gia_ManStop( pNew );
+    pFinal = Gia_ManEquivRemapDfs( pNew = pFinal );
+    Gia_ManStop( pNew );
     return pFinal;
 }
 
@@ -448,25 +564,24 @@ int Gia_ManEquivSetColor_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fOdds )
 int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
 {
     Gia_Obj_t * pObj;
-    int i, nNodes[2] = {0,0}, nDiffs[2];
+    int i, nNodes[2], nDiffs[2];
     assert( (Gia_ManPoNum(p) & 1) == 0 );
     Gia_ObjSetColors( p, 0 );
     Gia_ManForEachPi( p, pObj, i )
         Gia_ObjSetColors( p, Gia_ObjId(p,pObj) );
+    nNodes[0] = nNodes[1] = Gia_ManPiNum(p);
     Gia_ManForEachPo( p, pObj, i )
         nNodes[i&1] += Gia_ManEquivSetColor_rec( p, Gia_ObjFanin0(pObj), i&1 );
 //    Gia_ManForEachObj( p, pObj, i )
 //        if ( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) )
 //            assert( Gia_ObjColors(p, i) );
-    nDiffs[0] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[0]);
-    nDiffs[1] = Gia_ManCiNum(p) + Gia_ManAndNum(p) - (Gia_ManPiNum(p) + nNodes[1]);
+    nDiffs[0] = Gia_ManCandNum(p) - nNodes[0];
+    nDiffs[1] = Gia_ManCandNum(p) - nNodes[1];
     if ( fVerbose )
     {
         printf( "CI+AND = %7d  A = %7d  B = %7d  Ad = %7d  Bd = %7d  AB = %7d.\n", 
-            Gia_ManCiNum(p) + Gia_ManAndNum(p), 
-            Gia_ManPiNum(p) + nNodes[0], Gia_ManPiNum(p) + nNodes[1], 
-            nDiffs[0], nDiffs[1], 
-            Gia_ManCiNum(p) + Gia_ManAndNum(p) - nDiffs[0] - nDiffs[1] );
+            Gia_ManCandNum(p), nNodes[0], nNodes[1], nDiffs[0], nDiffs[1], 
+            Gia_ManCandNum(p) - nDiffs[0] - nDiffs[1] );
     }
     return (nDiffs[0] + nDiffs[1]) / 2;
 }
@@ -482,13 +597,16 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
 {
     Gia_Obj_t * pRepr;
     unsigned iLitNew;
     pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
     if ( pRepr == NULL )
         return;
+//    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+    if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+        return;
     iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
         Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
@@ -506,15 +624,15 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits )
+void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
-    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
+    Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
+    Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
 }
 
 /**Function*************************************************************
@@ -528,7 +646,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
+Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -539,9 +657,21 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
         printf( "Gia_ManSpecReduce(): Equivalence classes are not available.\n" );
         return NULL;
     }
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    {
+        printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
+        return NULL;
+    }
+    if ( !Gia_ManCheckTopoOrder( p ) )
+    {
+        printf( "Gia_ManSpecReduce(): AIG is not in a correct topological order.\n" );
+        return NULL;
+    }
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
+    if ( fDualOut )
+        Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
@@ -549,9 +679,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
     Gia_ManForEachRo( p, pObj, i )
-        Gia_ManSpecBuild( pNew, p, pObj, vXorLits );
+        Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits );
+        Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
     Vec_IntForEachEntry( vXorLits, iLitNew, i )
         Gia_ManAppendCo( pNew, iLitNew );
     if ( Vec_IntSize(vXorLits) == 0 )
@@ -570,12 +700,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut )
 }
 
 
-static inline int  Gia_ObjSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)];  }
-static inline void Gia_ObjSetSpec( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit;  }
-
-static inline int  Gia_ObjChild0Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
-static inline int  Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjSpec(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
-
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG in the DFS order.]
@@ -587,17 +711,20 @@ static inline int  Gia_ObjChild1Spec( Gia_Man_t * p, int f, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
 {
     Gia_Obj_t * pRepr;
     int iLitNew;
     pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
     if ( pRepr == NULL )
         return;
-    iLitNew = Gia_LitNotCond( Gia_ObjSpec(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-    if ( Gia_ObjSpec(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
-        Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjSpec(p, f, pObj), iLitNew) );
-    Gia_ObjSetSpec( p, f, pObj, iLitNew );
+//    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+    if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
+        return;
+    iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+    if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
+        Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
+    Gia_ObjSetCopyF( p, f, pObj, iLitNew );
 }
 
 /**Function*************************************************************
@@ -611,15 +738,15 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f )
+void Gia_ManSpecReduceInit_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int f, int fDualOut )
 {
-    if ( ~Gia_ObjSpec(p, f, pObj) )
+    if ( ~Gia_ObjCopyF(p, f, pObj) )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f );
-    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f );
-    Gia_ObjSetSpec( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjChild0Spec(p, f, pObj), Gia_ObjChild1Spec(p, f, pObj)) );
-    Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
+    Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, f, fDualOut );
+    Gia_ObjSetCopyF( p, f, pObj, Gia_ManHashAnd(pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj)) );
+    Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
 }
 
 /**Function*************************************************************
@@ -654,31 +781,43 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
         printf( "Gia_ManSpecReduceInit(): Mismatch in the number of registers.\n" );
         return NULL;
     }
+    if ( fDualOut && (Gia_ManPoNum(p) & 1) )
+    {
+        printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
+        return NULL;
+    }
+    if ( !Gia_ManCheckTopoOrder( p ) )
+    {
+        printf( "Gia_ManSpecReduceInit(): AIG is not in a correct topological order.\n" );
+        return NULL;
+    }
     assert( pInit->nRegs == Gia_ManRegNum(p) && pInit->nPis == 0 );
     p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
     vXorLits = Vec_IntAlloc( 1000 );
     Gia_ManSetPhase( p );
+    if ( fDualOut )
+        Gia_ManEquivSetColors( p, 0 );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
-        Gia_ObjSetSpec( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
+        Gia_ObjSetCopyF( p, 0, pObj, Aig_InfoHasBit(pInit->pData, i) );
     for ( f = 0; f < nFrames; f++ )
     {
-        Gia_ObjSetSpec( p, f, Gia_ManConst0(p), 0 );
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
         Gia_ManForEachPi( p, pObj, i )
-            Gia_ObjSetSpec( p, f, pObj, Gia_ManAppendCi(pNew) );
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
         Gia_ManForEachRo( p, pObj, i )
-            Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f );
+            Gia_ManSpecBuildInit( pNew, p, pObj, vXorLits, f, fDualOut );
         Gia_ManForEachCo( p, pObj, i )
         {
-            Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f );
-            Gia_ObjSetSpec( p, f, pObj, Gia_ObjChild0Spec(p, f, pObj) );
+            Gia_ManSpecReduceInit_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, f, fDualOut );
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ObjFanin0CopyF(p, f, pObj) );
         }
         if ( f == nFrames - 1 )
             break;
         Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
-            Gia_ObjSetSpec( p, f+1, pObjRo, Gia_ObjSpec(p, f, pObjRi) );
+            Gia_ObjSetCopyF( p, f+1, pObjRo, Gia_ObjCopyF(p, f, pObjRi) );
     }
     Vec_IntForEachEntry( vXorLits, iLitNew, i )
         Gia_ManAppendCo( pNew, iLitNew );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 3db3e396..f11345eb 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -92,7 +92,7 @@ static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  {
 /*=== sswAbs.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int fVerbose );
 /*=== saigBmc.c ==========================================================*/
-extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
+extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
 extern void              Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 8ba02528..f8799e38 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -173,16 +173,24 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
+int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit )
 {
+    extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit );
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pFrames, * pAigTemp;
     Aig_Obj_t * pObj;
     int status, clk, Lit, i, RetValue = 1;
+
     // derive the timeframes
     clk = clock();
-    if ( nSizeMax > 0 )
+    if ( nCofFanLit )
+    {
+        pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
+        if ( pFrames == NULL )
+            return -1;
+    }
+    else if ( nSizeMax > 0 )
     {
         pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
         nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 9d09d4e7..03df38e1 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -146,6 +146,18 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
     for ( nIter = 0; ; nIter++ )
     {
+        if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
+        {
+            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
+            Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
+            Aig_ManStop( pSRed );
+            printf( "Iterative refinement is stopped before iteration %d.\n", nIter );
+            printf( "The network is reduced using candidate equivalences.\n" );
+            printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
+            printf( "If the miter is SAT, the reduced result is incorrect.\n" );
+            break;
+        }
+
 clk = clock();
         p->pMSat = Ssw_SatStart( 0 );
         if ( p->pPars->fLatchCorrOpt )
@@ -199,18 +211,6 @@ clk = clock();
         Ssw_ManCleanup( p );
         if ( !RetValue ) 
             break;
-
-        if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
-        {
-            Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
-            Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
-            Aig_ManStop( pSRed );
-            printf( "Iterative refinement is stopped after iteration %d.\n", nIter );
-            printf( "The network is reduced using candidate equivalences.\n" );
-            printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" );
-            printf( "If the miter is SAT, the reduced result is incorrect.\n" );
-            break;
-        }
     } 
     p->pPars->nIters = nIter + 1;
 p->timeTotal = clock() - clkTotal;
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index b7fe6316..2869352c 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -661,6 +661,7 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames,
 /*=== abcNames.c ====================================================*/
 extern ABC_DLL char *             Abc_ObjName( Abc_Obj_t * pNode );
 extern ABC_DLL char *             Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
+extern ABC_DLL char *             Abc_ObjNamePrefix( Abc_Obj_t * pObj, char * pPrefix );
 extern ABC_DLL char *             Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
 extern ABC_DLL char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
 extern ABC_DLL void               Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index 19bdc47e..2addf289 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -40,9 +40,9 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter )
+void Abc_NtkFlattenLogicHierarchy2_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter )
 {
-    char Suffix[1000] = {0};
+    char Suffix[2000] = {0};
     Abc_Ntk_t * pNtkModel;
     Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin;
     int i, k;
@@ -70,7 +70,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
 
     (*pCounter)++;
 
-    // create the prefix, which will be appended to the internal names
+    // create the suffix, which will be appended to the internal names
     if ( *pCounter )
         sprintf( Suffix, "_%s_%d", Abc_NtkName(pNtk), *pCounter );
 
@@ -98,7 +98,18 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
     Abc_NtkForEachPi( pNtk, pTerm, i )
         Abc_NodeSetTravIdCurrent( pTerm );
     Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
         Abc_NodeSetTravIdCurrent( pTerm );
+        // if the netlist has net names beginning with "abc_property_"
+        // these names will be addes as primary outputs of the network
+        pNet = Abc_ObjFanin0(pTerm);
+        if ( strncmp( Abc_ObjName(pNet), "abc_property", 12 ) )
+            continue;
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNet->pCopy->pNtk), pNet->pCopy );
+        if ( Nm_ManFindNameById(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id) )
+            Nm_ManDeleteIdName(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id);
+        Abc_ObjAssignName( pNet->pCopy, Abc_ObjName(pNet), Suffix );
+    }
     Abc_NtkForEachBox( pNtk, pObj, i )
     {
         if ( Abc_ObjIsLatch(pObj) )
@@ -144,7 +155,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
         Abc_ObjForEachFanout( pObj, pTerm, k )
             Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy;
         // call recursively
-        Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter );
+        Abc_NtkFlattenLogicHierarchy2_rec( pNtkNew, pNtkModel, pCounter );
     }
 
     // if it is a BLIF-MV netlist transfer the values of all nets
@@ -168,7 +179,7 @@ void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, in
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy2( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pTerm, * pNet;
@@ -203,7 +214,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
 
     // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
     Counter = -1;
-    Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter );
+    Abc_NtkFlattenLogicHierarchy2_rec( pNtkNew, pNtk, &Counter );
     printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", 
         Counter, Abc_NtkBlackboxNum(pNtkNew) );
 
@@ -217,6 +228,241 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
             pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
     }
 
+    // we may have added property outputs
+    Abc_NtkOrderCisCos( pNtkNew );
+
+    // copy the timing information
+//    Abc_ManTimeDup( pNtk, pNtkNew );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        printf( "EXDC is not transformed.\n" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        fprintf( stdout, "Abc_NtkFlattenLogicHierarchy2(): Network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively flattens logic hierarchy of the netlist.]
+
+  Description [When this procedure is called, the PI/PO nets of the old 
+  netlist point to the corresponding nets of the flattened netlist.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFlattenLogicHierarchy_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int * pCounter, Vec_Str_t * vPref )
+{
+    Abc_Ntk_t * pNtkModel;
+    Abc_Obj_t * pObj, * pTerm, * pNet, * pFanin;
+    int i, k, Length;
+
+    // process the blackbox
+    if ( Abc_NtkHasBlackbox(pNtk) )
+    {
+        // duplicate the blackbox
+        assert( Abc_NtkBoxNum(pNtk) == 1 );
+        pObj = Abc_NtkBox( pNtk, 0 );
+        Abc_NtkDupBox( pNtkNew, pObj, 1 );
+        pObj->pCopy->pData = pNtk;
+
+        // connect blackbox fanins to the PI nets
+        assert( Abc_ObjFaninNum(pObj->pCopy) == Abc_NtkPiNum(pNtk) );
+        Abc_NtkForEachPi( pNtk, pTerm, i )
+            Abc_ObjAddFanin( Abc_ObjFanin(pObj->pCopy,i), Abc_ObjFanout0(pTerm)->pCopy );
+
+        // connect blackbox fanouts to the PO nets
+        assert( Abc_ObjFanoutNum(pObj->pCopy) == Abc_NtkPoNum(pNtk) );
+        Abc_NtkForEachPo( pNtk, pTerm, i )
+            Abc_ObjAddFanin( Abc_ObjFanin0(pTerm)->pCopy, Abc_ObjFanout(pObj->pCopy,i) );
+        return;
+    }
+
+    (*pCounter)++;
+
+    // create the suffix, which will be appended to the internal names
+    if ( *pCounter )
+    {
+        char Buffer[20];
+        sprintf( Buffer, "(%d)", *pCounter );
+        Vec_StrAppend( vPref, Buffer );
+    }
+    Vec_StrPush( vPref, '|' );
+    Vec_StrPush( vPref, 0 );
+
+    // duplicate nets of all boxes, including latches
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+        {
+            pNet = Abc_ObjFanin0(pTerm);
+            if ( pNet->pCopy )
+                continue;
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNamePrefix(pNet, Vec_StrArray(vPref)) );
+        }
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+        {
+            pNet = Abc_ObjFanout0(pTerm);
+            if ( pNet->pCopy )
+                continue;
+            pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjNamePrefix(pNet, Vec_StrArray(vPref)) );
+        }
+    }
+
+    // mark objects that will not be used
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+        Abc_NodeSetTravIdCurrent( pTerm );
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        Abc_NodeSetTravIdCurrent( pTerm );
+        // if the netlist has net names beginning with "abc_property_"
+        // these names will be addes as primary outputs of the network
+        pNet = Abc_ObjFanin0(pTerm);
+        if ( strncmp( Abc_ObjName(pNet), "abc_property", 12 ) )
+            continue;
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pNet->pCopy->pNtk), pNet->pCopy );
+        if ( Nm_ManFindNameById(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id) )
+            Nm_ManDeleteIdName(pNet->pCopy->pNtk->pManName, pNet->pCopy->Id);
+        Abc_ObjAssignName( pNet->pCopy, Vec_StrArray(vPref), Abc_ObjName(pNet) );
+    }
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        Abc_NodeSetTravIdCurrent( pObj );
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_NodeSetTravIdCurrent( pTerm );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_NodeSetTravIdCurrent( pTerm );
+    }
+
+    // duplicate objects that do not have prototypes yet
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            continue;
+        if ( pObj->pCopy )
+            continue;
+        Abc_NtkDupObj( pNtkNew, pObj, 0 );
+    }
+
+    // connect objects
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent(pObj) )
+            Abc_ObjForEachFanin( pObj, pFanin, k )
+                if ( !Abc_NodeIsTravIdCurrent(pFanin) )
+                    Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+
+    // call recursively
+    Vec_StrPop( vPref );
+    Length = Vec_StrSize( vPref );
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        pNtkModel = pObj->pData;
+        // check the match between the number of actual and formal parameters
+        assert( Abc_ObjFaninNum(pObj) == Abc_NtkPiNum(pNtkModel) );
+        assert( Abc_ObjFanoutNum(pObj) == Abc_NtkPoNum(pNtkModel) );
+        // clean the node copy fields
+        Abc_NtkCleanCopy( pNtkModel );
+        // map PIs/POs
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Abc_ObjFanout0( Abc_NtkPi(pNtkModel, k) )->pCopy = Abc_ObjFanin0(pTerm)->pCopy;
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Abc_ObjFanin0( Abc_NtkPo(pNtkModel, k) )->pCopy = Abc_ObjFanout0(pTerm)->pCopy;
+        // create name
+        Vec_StrShrink( vPref, Length );
+        Vec_StrAppend( vPref, Abc_NtkName(pNtkModel) );
+        // call recursively
+        Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtkModel, pCounter, vPref );
+    }
+
+    // if it is a BLIF-MV netlist transfer the values of all nets
+    if ( Abc_NtkHasBlifMv(pNtk) && Abc_NtkMvVar(pNtk) )
+    {
+        if ( Abc_NtkMvVar( pNtkNew ) == NULL )
+            Abc_NtkStartMvVars( pNtkNew );
+        Abc_NtkForEachNet( pNtk, pObj, i )
+            Abc_NtkSetMvVarValues( pObj->pCopy, Abc_ObjMvVarNum(pObj) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Flattens the logic hierarchy of the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
+{
+    extern Abc_Lib_t * Abc_LibDupBlackboxes( Abc_Lib_t * pLib, Abc_Ntk_t * pNtkSave );
+    Vec_Str_t * vPref;
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pTerm, * pNet;
+    int i, Counter = -1;
+
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+
+    // clean the node copy fields
+    Abc_NtkCleanCopy( pNtk );
+
+    // duplicate PIs/POs and their nets
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+    {
+        Abc_NtkDupObj( pNtkNew, pTerm, 0 );
+        pNet = Abc_ObjFanout0( pTerm );
+        pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+        Abc_ObjAddFanin( pNet->pCopy, pTerm->pCopy );
+    }
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        Abc_NtkDupObj( pNtkNew, pTerm, 0 );
+        pNet = Abc_ObjFanin0( pTerm );
+        pNet->pCopy = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pNet) );
+        Abc_ObjAddFanin( pTerm->pCopy, pNet->pCopy );
+    }
+
+    // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
+    vPref = Vec_StrAlloc( 1000 );
+    Vec_StrAppend( vPref, Abc_NtkName(pNtk) );
+    Abc_NtkFlattenLogicHierarchy_rec( pNtkNew, pNtk, &Counter, vPref );
+    printf( "Hierarchy reader flattened %d instances of logic boxes and left %d black boxes.\n", 
+        Counter, Abc_NtkBlackboxNum(pNtkNew) );
+    Vec_StrFree( vPref );
+
+    if ( pNtk->pDesign )
+    {
+        // pass on the design
+        assert( Vec_PtrEntry(pNtk->pDesign->vTops, 0) == pNtk );
+        pNtkNew->pDesign = Abc_LibDupBlackboxes( pNtk->pDesign, pNtkNew );
+        // update the pointers
+        Abc_NtkForEachBlackbox( pNtkNew, pTerm, i )
+            pTerm->pData = ((Abc_Ntk_t *)pTerm->pData)->pCopy;
+    }
+
+    // we may have added property outputs
+    Abc_NtkOrderCisCos( pNtkNew );
+
     // copy the timing information
 //    Abc_ManTimeDup( pNtk, pNtkNew );
     // duplicate EXDC 
@@ -231,6 +477,7 @@ Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk )
     return pNtkNew;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Extracts blackboxes by making them into additional PIs/POs.]
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 90fcd191..e07b47c1 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -70,9 +70,27 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix )
 
 /**Function*************************************************************
 
-  Synopsis    [Gets the long name of the node.]
+  Synopsis    [Appends name to the prefix]
 
-  Description [This name is the output net's name.]
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_ObjNamePrefix( Abc_Obj_t * pObj, char * pPrefix )
+{
+    static char Buffer[2000];
+    sprintf( Buffer, "%s%s", pPrefix, Abc_ObjName(pObj) );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Appends suffic to the name.]
+
+  Description []
                
   SideEffects []
 
@@ -81,7 +99,7 @@ char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix )
 ***********************************************************************/
 char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix )
 {
-    static char Buffer[500];
+    static char Buffer[2000];
     sprintf( Buffer, "%s%s", Abc_ObjName(pObj), pSuffix );
     return Buffer;
 }
@@ -99,7 +117,7 @@ char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix )
 ***********************************************************************/
 char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
 {
-    static char Buffer[100];
+    static char Buffer[2000];
     sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
     return Buffer;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3045eb93..b5e23856 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17580,9 +17580,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nNodeDelta;
     int fRewrite;
     int fNewAlgo;
+    int nCofFanLit;
     int fVerbose;
 
-    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -17596,9 +17597,10 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     nNodeDelta  =     1000;
     fRewrite    =        0;
     fNewAlgo    =        1;
+    nCofFanLit  =        0;
     fVerbose    =        0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDLrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -17657,6 +17659,17 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nNodeDelta < 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCofFanLit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCofFanLit < 0 ) 
+                goto usage;
+            break;
         case 'r':
             fRewrite ^= 1;
             break;
@@ -17687,19 +17700,20 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Does not work for combinational networks.\n" );
         return 0;
     }
-    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, nCofFanLit, fVerbose );
     pAbc->pCex = pNtk->pSeqModel; // temporary ???
     return 0;
 
 usage:
 //    fprintf( pErr, "usage: bmc [-FNCGD num] [-ravh]\n" );
-    fprintf( pErr, "usage: bmc [-FNC num] [-rvh]\n" );
+    fprintf( pErr, "usage: bmc [-FNCL num] [-rcvh]\n" );
     fprintf( pErr, "\t         performs bounded model checking with static unrolling\n" );
     fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
     fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
 //    fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll );
 //    fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta );
+    fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
 //    fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -17732,7 +17746,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fNewAlgo;
     int fVerbose;
 
-    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -17837,7 +17851,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Does not work for combinational networks.\n" );
         return 0;
     }
-    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, 0, fVerbose );
     pAbc->pCex = pNtk->pSeqModel; // temporary ???
     return 0;
 
@@ -22007,7 +22021,7 @@ usage:
 int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
-    int fSetReset = 0;
+    int fSetReset = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
     {
@@ -22032,7 +22046,7 @@ int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9PSigs(): Works only for sequential circuits.\n" );
         return 1;
     } 
-    Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset );
+    Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset, 1 );
     return 0;
 
 usage:
@@ -22233,9 +22247,10 @@ usage:
 int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
-    int c, iVar = 0, nLimFan = 0;
+    int c, fVerbose = 0;
+    int iVar = 0, nLimFan = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "VLh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "VLvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22255,12 +22270,15 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
             {
                 fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
                 goto usage;
-            }
+            } 
             nLimFan = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             if ( nLimFan < 0 ) 
                 goto usage;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22272,7 +22290,21 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManDupCofactored( pTemp = pAbc->pAig, iVar, nLimFan );
+    if ( nLimFan )
+    {
+        printf( "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
+        pAbc->pAig = Gia_ManDupCofAll( pTemp = pAbc->pAig, nLimFan, fVerbose );
+    }
+    else if ( iVar )
+    {
+        printf( "Cofactoring one variable with object ID %d.\n", iVar );
+        pAbc->pAig = Gia_ManDupCof( pTemp = pAbc->pAig, iVar );
+    }
+    else
+    {
+        printf( "One of the paramters, -V <num> or -L <num>, should be set on the command line.\n" );
+        goto usage;
+    }
     if ( pAbc->pAig == NULL )
     {
         pAbc->pAig = pTemp;
@@ -22283,10 +22315,11 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &cof [-VL num] [-h]\n" );
-    fprintf( stdout, "\t         performs cofactoring w.r.t. a variable\n" );
-    fprintf( stdout, "\t-V num : the zero-based ID of the variable to cofactor [default = %d]\n", iVar );
-    fprintf( stdout, "\t-L num : cofactor w.r.t. variables whose fanout is higher [default = %d]\n", nLimFan );
+    fprintf( stdout, "usage: &cof [-VL num] [-vh]\n" );
+    fprintf( stdout, "\t         performs cofactoring w.r.t. variable(s)\n" );
+    fprintf( stdout, "\t-V num : the zero-based ID of one variable to cofactor [default = %d]\n", iVar );
+    fprintf( stdout, "\t-L num : cofactor vars with fanout count higher than this [default = %d]\n", nLimFan );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -22825,9 +22858,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp;
     Gia_ParFra_t Pars, * pPars = &Pars;
     int c;
+    int nCofFanLit = 0;
     Gia_ManFraSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FLivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22842,6 +22876,17 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFrames < 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCofFanLit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCofFanLit < 0 ) 
+                goto usage;
+            break;
         case 'i':
             pPars->fInit ^= 1;
             break;
@@ -22859,14 +22904,18 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Times(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars );
+    if ( nCofFanLit )
+        pAbc->pAig = Gia_ManUnrollAndCofactor( pTemp = pAbc->pAig, pPars->nFrames, nCofFanLit, pPars->fVerbose );
+    else
+        pAbc->pAig = Gia_ManFrames( pTemp = pAbc->pAig, pPars );
     Gia_ManStop( pTemp );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &frames [-F <num>] [-ivh]\n" );
+    fprintf( stdout, "usage: &frames [-FL <num>] [-ivh]\n" );
     fprintf( stdout, "\t         unrolls the design for several timeframes\n" );
     fprintf( stdout, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
     fprintf( stdout, "\t-i     : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
@@ -22929,7 +22978,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         pAbc->pAig = Gia_ManTransformMiter( pAux = pAbc->pAig );
         Gia_ManStop( pAux );
-        printf( "Abc_CommandAbc9Miter(): Miter is transformed by merging POs pair-wise.\n" );
+        printf( "The miter (current AIG) is transformed by XORing POs pair-wise.\n" );
         return 0;
     }
 
@@ -23286,7 +23335,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    char * pFileName = "gia_srm.aig";
+    char * pFileName = "gsrm.aig";
     Gia_Man_t * pTemp;
     int c, fVerbose = 0;
     int fDualOut = 0;
@@ -23314,11 +23363,14 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     } 
 //    pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
 //    Gia_ManStop( pTemp );
-    pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut );
-    Gia_WriteAiger( pTemp, "gia_srm.aig", 0, 0 );
-    printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
-    Gia_ManPrintStatsShort( pTemp );
-    Gia_ManStop( pTemp );
+    pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose );
+    if ( pTemp )
+    {
+        Gia_WriteAiger( pTemp, pFileName, 0, 0 );
+        printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
+        Gia_ManPrintStatsShort( pTemp );
+        Gia_ManStop( pTemp );
+    }
     return 0;
 
 usage:
@@ -23346,14 +23398,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp;
     int c, fVerbose = 0;
     int fUseAll = 0;
+    int fDualOut = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "avh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "advh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'a':
             fUseAll ^= 1;
             break;
+        case 'd':
+            fDualOut ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -23368,14 +23424,18 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Reduce(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll );
-    Gia_ManStop( pTemp );
+    pAbc->pAig = Gia_ManEquivReduce( pTemp = pAbc->pAig, fUseAll, fDualOut, fVerbose );
+    if ( pAbc->pAig == NULL )
+        pAbc->pAig = pTemp;
+    else
+        Gia_ManStop( pTemp );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &reduce [-avh]\n" );
+    fprintf( stdout, "usage: &reduce [-advh]\n" );
     fprintf( stdout, "\t         reduces the circuit using equivalence classes\n" );
-    fprintf( stdout, "\t-a     : toggle creating dual output miter [default = %s]\n", fUseAll? "yes": "no" );
+    fprintf( stdout, "\t-a     : toggle merging all equivalences [default = %s]\n", fUseAll? "yes": "no" );
+    fprintf( stdout, "\t-d     : toggle using dual-output merging [default = %s]\n", fDualOut? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -23922,6 +23982,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManTestDistance( pAbc->pAig );
 //    Gia_SatSolveTest( pAbc->pAig );
 //    For_ManExperiment( pAbc->pAig, 20, 1, 1 );
+//    Gia_ManUnrollSpecial( pAbc->pAig, 5, 100, 1 );
+    pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
     return 0;
 
 usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ca33667f..91046340 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1538,7 +1538,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose )
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int nCofFanLit, int fVerbose )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
@@ -1554,7 +1554,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
     if ( fNewAlgo )
     {
         int iFrame;
-        RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame );
+        RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit );
         ABC_FREE( pNtk->pModel );
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
@@ -1751,7 +1751,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     }
     if ( pSecPar->fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0 );
+        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0, 0 );
         if ( RetValue == 0 )
         {
             printf( "Networks are not equivalent.\n" );
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index dcabaf36..7761d428 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -91,7 +91,7 @@ int main( int argc, char * argv[] )
     {
         // perform BMC
         if ( pAig->nRegs != 0 )
-            RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
+            RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 );
 
         // perform full-blown SEC
         if ( RetValue != 0 )
@@ -120,7 +120,7 @@ int main( int argc, char * argv[] )
         int nSizeMax = 500000;
         int nBTLimit = 10000000;
         int fRewrite = 0;
-        RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth );
+        RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 );
         if ( RetValue != 0 )
             RetValue = -1;
     }