Version abc90424

33 files changed, 2092 insertions, 122 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 63db3c01..c3f70016 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2959,6 +2959,10 @@ SOURCE=.\src\aig\aig\aigDup.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigFact.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigFanout.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aigFact.c b/src/aig/aig/aigFact.c
new file mode 100644
index 00000000..7004618a
--- /dev/null
+++ b/src/aig/aig/aigFact.c
@@ -0,0 +1,272 @@
+/**CFile****************************************************************
+
+  FileName    [aigFactor.c]
+
+  SystemName  []
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation []
+
+  Date        [Ver. 1.0. Started - April 17, 2009.]
+
+  Revision    [$Id: aigFactor.c,v 1.00 2009/04/17 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Detects multi-input AND gate rooted at this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFindImplications_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vImplics )
+{
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) )
+    {
+        Vec_PtrPushUnique( vImplics, pObj );
+        return;
+    }
+    Aig_ManFindImplications_rec( Aig_ObjChild0(pObj), vImplics );
+    Aig_ManFindImplications_rec( Aig_ObjChild1(pObj), vImplics );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the nodes whose values are implied by pNode.]
+
+  Description [Attention!  Both pNode and results can be complemented!
+  Also important: Currently, this procedure only does backward propagation. 
+  In general, it may find more implications if forward propagation is enabled.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManFindImplications( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+    Vec_Ptr_t * vImplics;
+    vImplics = Vec_PtrAlloc( 100 );
+    Aig_ManFindImplications_rec( pNode, vImplics );
+    return vImplics;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cone of the node overlaps with the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManFindConeOverlap_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+    if ( Aig_ObjIsTravIdPrevious( p, pNode ) )
+        return 1;
+    if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pNode );
+    if ( Aig_ObjIsPi(pNode) )
+        return 0;
+    if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin0(pNode) ) )
+        return 1;
+    if ( Aig_ManFindConeOverlap_rec( p, Aig_ObjFanin1(pNode) ) )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cone of the node overlaps with the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManFindConeOverlap( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode )
+{
+    Aig_Obj_t * pTemp;
+    int i;
+    assert( !Aig_IsComplement(pNode) );
+    assert( !Aig_ObjIsConst1(pNode) );
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vImplics, pTemp, i )
+        Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
+    Aig_ManIncrementTravId( p );
+    return Aig_ManFindConeOverlap_rec( p, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cone of the node overlaps with the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDeriveNewCone_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+    if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
+        return pNode->pData;
+    Aig_ObjSetTravIdCurrent( p, pNode );
+    if ( Aig_ObjIsPi(pNode) )
+        return pNode->pData = pNode;
+    Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin0(pNode) );
+    Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin1(pNode) );
+    return pNode->pData = Aig_And( p, Aig_ObjChild0Copy(pNode), Aig_ObjChild1Copy(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cone of the node overlaps with the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDeriveNewCone( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNode )
+{
+    Aig_Obj_t * pTemp;
+    int i;
+    assert( !Aig_IsComplement(pNode) );
+    assert( !Aig_ObjIsConst1(pNode) );
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vImplics, pTemp, i )
+    {
+        Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
+        Aig_Regular(pTemp)->pData = Aig_NotCond( Aig_ManConst1(p), Aig_IsComplement(pTemp) );
+    }
+    return Aig_ManDeriveNewCone_rec( p, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns algebraic factoring of B in terms of A.]
+
+  Description [Returns internal node C (an AND gate) that is equal to B 
+  under assignment A = 'Value', or NULL if there is no such node C. ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManFactorAlgebraic_int( Aig_Man_t * p, Aig_Obj_t * pPoA, Aig_Obj_t * pPoB, int Value )
+{
+    Aig_Obj_t * pNodeA, * pNodeC;
+    Vec_Ptr_t * vImplics;
+    int RetValue;
+    if ( Aig_ObjIsConst1(Aig_ObjFanin0(pPoA)) || Aig_ObjIsConst1(Aig_ObjFanin0(pPoB)) )
+        return NULL;
+    if ( Aig_ObjIsPi(Aig_ObjFanin0(pPoB)) )
+        return NULL;
+    // get the internal node representing function of A under assignment A = 'Value'
+    pNodeA = Aig_ObjChild0( pPoA );
+    pNodeA = Aig_NotCond( pNodeA, Value==0 );
+    // find implications of this signal (nodes whose value is fixed under assignment A = 'Value')
+    vImplics = Aig_ManFindImplications( p, pNodeA );
+    // check if the TFI cone of B overlaps with the implied nodes
+    RetValue = Aig_ManFindConeOverlap( p, vImplics, Aig_ObjFanin0(pPoB) );
+    if ( RetValue == 0 ) // no overlap
+    {
+        Vec_PtrFree( vImplics );
+        return NULL;
+    }
+    // there is overlap - derive node representing value of B under assignment A = 'Value'
+    pNodeC = Aig_ManDeriveNewCone( p, vImplics, Aig_ObjFanin0(pPoB) );
+    pNodeC = Aig_NotCond( pNodeC, Aig_ObjFaninC0(pPoB) );
+    Vec_PtrFree( vImplics );
+    return pNodeC;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns algebraic factoring of B in terms of A.]
+
+  Description [Returns internal node C (an AND gate) that is equal to B 
+  under assignment A = 'Value', or NULL if there is no such node C. ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManFactorAlgebraic( Aig_Man_t * p, int iPoA, int iPoB, int Value )
+{
+    assert( iPoA >= 0 && iPoA < Aig_ManPoNum(p) );
+    assert( iPoB >= 0 && iPoB < Aig_ManPoNum(p) );
+    assert( Value == 0 || Value == 1 );
+    return Aig_ManFactorAlgebraic_int( p, Aig_ManPo(p, iPoA), Aig_ManPo(p, iPoB), Value ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFactorAlgebraicTest( Aig_Man_t * p )
+{
+    int iPoA  = 0;
+    int iPoB  = 1;
+    int Value = 0;
+    Aig_Obj_t * pRes;
+//    Aig_Obj_t * pObj;
+//    int i;
+    pRes = Aig_ManFactorAlgebraic( p, iPoA, iPoB, Value );
+    Aig_ManShow( p, 0, NULL );
+    Aig_ObjPrint( p, pRes );
+    printf( "\n" );
+/*
+    printf( "Results:\n" );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        printf( "Object = %d.\n", i );
+        Aig_ObjPrint( p, pObj );
+        printf( "\n" );
+        Aig_ObjPrint( p, pObj->pData );
+        printf( "\n" );
+    }
+*/
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 8d243419..9034f272 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -313,6 +313,16 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
     int fHaig = 0;
     int fShowFanouts = 0;
     Aig_Obj_t * pTemp;
+    if ( pObj == NULL )
+    {
+        printf( "Object is NULL." );
+        return;
+    }
+    if ( Aig_IsComplement(pObj) )
+    {
+        printf( "Compl " );
+        pObj = Aig_Not(pObj);
+    }
     assert( !Aig_IsComplement(pObj) );
     printf( "Node %4d : ", Aig_ObjId(pObj) );
     if ( Aig_ObjIsConst1(pObj) )
diff --git a/src/aig/bbl/bblif.h b/src/aig/bbl/bblif.h
index db3eb2f5..89c58f93 100644
--- a/src/aig/bbl/bblif.h
+++ b/src/aig/bbl/bblif.h
@@ -36,6 +36,14 @@
     (3) read a binary BLIF file with a mapped network produced by ABC
     (4) return the mapped network to the caller through a set of APIs
 
+    It should be noted that the BBLIF interface can be used to pass
+    the network from the calling application into ABC without writing it
+    into a file. In this case, ABC should be compiled as a library and
+    linked to the calling application. The BBLIF manager can be given
+    directly to the procedure Bbl_ManToAbc() to convert it into an AIG.
+    Similarly, the resulting mapped network can be converted into
+    BBLIF manager and passed back after the call to Bbl_ManFromAbc().
+
     Here these steps are described in more detail:
 
     (1) The BBLIF manager is allocated by calling Bbl_ManStart() and 
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 5cb8d345..8e14d2ef 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -122,6 +122,7 @@ struct Cec_ParCor_t_
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
     int              nFrames;       // the number of time frames
+    int              nPrefix;       // the number of time frames in the prefix
     int              nBTLimit;      // conflict limit at a node
     int              fLatchCorr;    // consider only latch outputs
     int              fUseRings;     // use rings
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index 7ec3dad4..111cc8a8 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -236,6 +236,33 @@ int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Implementation of new signal correspodence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat )
+{
+    extern int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
+    Gia_Man_t * pGia;
+    Cec_ParCor_t CorPars, * pCorPars = &CorPars;
+    Cec_ManCorSetDefaultParams( pCorPars );
+    pCorPars->fUseCSat  = fUseCSat;
+    pCorPars->nBTLimit  = nConfs;
+    pGia = Gia_ManFromAigSimple( pAig );
+    Cec_ManLSCorrespondenceClasses( pGia, pCorPars );
+    Gia_ManReprToAigRepr( pAig, pGia );
+    Gia_ManStop( pGia );
+    return Aig_ManDupSimple( pAig );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index cd3ce7b9..fd723f30 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -712,6 +712,8 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
         pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
         pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
 
+//        printf( "%d,%d  ", Gia_ObjValue( Gia_ObjFanin0(pObj) ), Gia_ObjValue( Gia_ObjFanin1(pObj) ) );
+
         if ( Gia_ObjFaninC0(pObj) )
         {
             if ( Gia_ObjFaninC1(pObj) )
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 8e97e207..b4076916 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f );
+static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,12 +41,12 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f )
+static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
 {
     if ( Gia_ObjIsAnd(pObj) )
     {
-        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f );
-        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f );
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
         return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
     }
     if ( f == 0 )
@@ -56,7 +56,7 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
     }
     assert( f && Gia_ObjIsRo(p, pObj) );
     pObj = Gia_ObjRoToRi( p, pObj );
-    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 );
+    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
     return Gia_ObjFanin0CopyF( p, f-1, pObj );
 }
 
@@ -71,21 +71,21 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f )
+void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
 {
     Gia_Obj_t * pRepr;
     int iLitNew;
     if ( ~Gia_ObjCopyF(p, f, pObj) )
         return;
-    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
     {
-        Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
+        Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
         iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
         Gia_ObjSetCopyF( p, f, pObj, iLitNew );
         return;
     }
     assert( Gia_ObjIsCand(pObj) );
-    iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
+    iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
     Gia_ObjSetCopyF( p, f, pObj, iLitNew );
 }
 
@@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
         {
             if ( Gia_ObjIsConst( p, i ) )
             {
-                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
+                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
                 iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
                 if ( iObjNew != 0 )
                 {
@@ -148,8 +148,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
                 iPrev = i;
                 Gia_ClassForEachObj1( p, i, iObj )
                 {
-                    iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
-                    iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
+                    iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                    iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
                     iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                     iObjNew  = Gia_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
                     if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
@@ -161,8 +161,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
                     iPrev = iObj;
                 }
                 iObj = i;
-                iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
-                iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
+                iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
                 iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                 iObjNew  = Gia_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
                 if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
@@ -181,8 +181,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
             pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
             if ( pRepr == NULL )
                 continue;
-            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames );
-            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
             iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
             if ( iPrevNew != iObjNew )
             {
@@ -216,18 +216,18 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
+Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pRepr;
     Vec_Int_t * vXorLits;
     int f, i, iPrevNew, iObjNew;
-    assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) );
+    assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
     assert( Gia_ManRegNum(p) > 0 );
     assert( p->pReprs != NULL );
-    p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
+    p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
     Gia_ManSetPhase( p );
-    pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+    pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
@@ -235,7 +235,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V
         Gia_ManAppendCi(pNew);
         Gia_ObjSetCopyF( p, 0, pObj, 0 );
     }
-    for ( f = 0; f < nFrames+fScorr; f++ )
+    for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
     { 
         Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
         Gia_ManForEachPi( p, pObj, i )
@@ -243,15 +243,15 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V
     }
     *pvOutputs = Vec_IntAlloc( 1000 );
     vXorLits = Vec_IntAlloc( 1000 );
-    for ( f = 0; f < nFrames; f++ )
+    for ( f = nPrefix; f < nFrames+nPrefix; f++ )
     {
         Gia_ManForEachObj1( p, pObj, i )
         {
             pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
             if ( pRepr == NULL )
                 continue;
-            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f );
-            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f );
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
             iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
             if ( iPrevNew != iObjNew )
             {
@@ -752,6 +752,74 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
 
 /**Function*************************************************************
 
+  Synopsis    [Runs BMC for the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
+{  
+    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+    Vec_Str_t * vStatus;
+    Vec_Int_t * vOutputs;
+    Vec_Int_t * vCexStore;
+    Cec_ManSim_t * pSim;
+    Gia_Man_t * pSrm;
+    int fChanges, RetValue;
+    // prepare simulation manager
+    Cec_ManSimSetDefaultParams( pParsSim );
+    pParsSim->nWords     = pPars->nWords;
+    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->fVerbose   = pPars->fVerbose;
+    pParsSim->fLatchCorr = pPars->fLatchCorr;
+    pParsSim->fSeqSimulate = 1;
+    pSim = Cec_ManSimStart( pAig, pParsSim );
+    // prepare SAT solving
+    Cec_ManSatSetDefaultParams( pParsSat );
+    pParsSat->nBTLimit = pPars->nBTLimit;
+    pParsSat->fVerbose = pPars->fVerbose;
+    fChanges = 1;
+    while ( fChanges )
+    {
+        int clkBmc = clock();
+        fChanges = 0;
+        pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+        if ( Gia_ManPoNum(pSrm) == 0 )
+        {
+            Gia_ManStop( pSrm );
+            Vec_IntFree( vOutputs );
+            break;
+        } 
+        pParsSat->nBTLimit *= 10;
+        if ( pPars->fUseCSat )
+            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+        else
+            vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+        // refine classes with these counter-examples
+        if ( Vec_IntSize(vCexStore) )
+        {
+            RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
+            Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+            fChanges = 1;
+        }
+        if ( pPars->fVerbose )
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+        // recycle
+        Vec_IntFree( vCexStore );
+        Vec_StrFree( vStatus );
+        Gia_ManStop( pSrm );
+        Vec_IntFree( vOutputs );
+    }
+    Cec_ManSimStop( pSim );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Internal procedure for register correspondence.]
 
   Description []
@@ -775,8 +843,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     int r, RetValue, clkTotal = clock();
     int clkSat = 0, clkSim = 0, clkSrm = 0;
     int clk2, clk = clock();
-    ABC_FREE( pAig->pReprs );
-    ABC_FREE( pAig->pNexts );
     if ( Gia_ManRegNum(pAig) == 0 )
     {
         printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
@@ -792,8 +858,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     pParsSim->fSeqSimulate = 1;
     // create equivalence classes of registers
     pSim = Cec_ManSimStart( pAig, pParsSim );
-    Cec_ManSimClassesPrepare( pSim );
-    Cec_ManSimClassesRefine( pSim );
+    if ( pAig->pReprs == NULL )
+    {
+        Cec_ManSimClassesPrepare( pSim );
+        Cec_ManSimClassesRefine( pSim );
+    }
     // prepare SAT solving
     Cec_ManSatSetDefaultParams( pParsSat );
     pParsSat->nBTLimit = pPars->nBTLimit;
@@ -805,6 +874,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
         Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
     }
+    // check the base case
+    if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
+            Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
     // perform refinement of equivalence classes
     for ( r = 0; r < nIterMax; r++ )
     { 
@@ -848,49 +920,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         Vec_IntFree( vOutputs );
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
     }
-    // check the base case
-    if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
-    {
-        int fChanges = 1;
-        while ( fChanges )
-        {
-            int clkBmc = clock();
-            fChanges = 0;
-            pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
-            if ( Gia_ManPoNum(pSrm) == 0 )
-            {
-                Gia_ManStop( pSrm );
-                Vec_IntFree( vOutputs );
-                break;
-            }
-            pParsSat->nBTLimit *= 10;
-            if ( pPars->fUseCSat )
-                vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
-            else
-                vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
-            // refine classes with these counter-examples
-            if ( Vec_IntSize(vCexStore) )
-            {
-                clk2 = clock();
-                RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
-                clkSim += clock() - clk2;
-                Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
-                fChanges = 1;
-            }
-            if ( pPars->fVerbose )
-                Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
-            // recycle
-            Vec_IntFree( vCexStore );
-            Vec_StrFree( vStatus );
-            Gia_ManStop( pSrm );
-            Vec_IntFree( vOutputs );
-        }
-    }
-    else
-    {
-        if ( pPars->fVerbose )
-            Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
-    }
+    if ( pPars->fVerbose )
+        Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
     // check the overflow
     if ( r == nIterMax )
         printf( "The refinement was not finished. The result may be incorrect.\n" );
@@ -910,6 +941,51 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes new initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
+{  
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    unsigned * pInitState;
+    int i, f; 
+    Gia_ManRandom( 1 );
+//    printf( "Simulating %d timeframes.\n", nFrames );
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark1 = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManConst0(pAig)->fMark1 = 0;
+        Gia_ManForEachPi( pAig, pObj, i )
+            pObj->fMark1 = Gia_ManRandom(0) & 1;
+        Gia_ManForEachAnd( pAig, pObj, i )
+            pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & 
+                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachRi( pAig, pObj, i )
+            pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
+            pObjRo->fMark1 = pObjRi->fMark1;
+    }
+    pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) );
+    Gia_ManForEachRo( pAig, pObj, i )
+    {
+        if ( pObj->fMark1 )
+            Gia_InfoSetBit( pInitState, i );
+//        printf( "%d", pObj->fMark1 );
+    }
+//    printf( "\n" );
+    Gia_ManCleanMark1( pAig );
+    return pInitState;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Top-level procedure for register correspondence.]
 
   Description []
@@ -922,8 +998,39 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 {  
     Gia_Man_t * pNew, * pTemp;
+    unsigned * pInitState;
     int RetValue;
-    RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
+    ABC_FREE( pAig->pReprs );
+    ABC_FREE( pAig->pNexts );
+    if ( pPars->nPrefix == 0 )
+        RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
+    else
+    {
+        // compute the cycles AIG
+        pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
+        pTemp = Gia_ManDupFlip( pAig, pInitState );
+        ABC_FREE( pInitState );
+        // compute classes of this AIG
+        RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
+        // transfer the class info
+        pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
+        pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
+        // perform additional BMC
+        pPars->fUseCSat = 0;
+        pPars->nBTLimit = ABC_MAX( pPars->nBTLimit, 1000 );
+        Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix );
+/*
+        // transfer the class info back
+        pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL;
+        pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL;
+        // continue refining
+        RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
+        // transfer the class info
+        pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
+        pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
+*/
+        Gia_ManStop( pTemp );
+    }
     // derive reduced AIG
     if ( pPars->fMakeChoices )
     {
@@ -932,7 +1039,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     }
     else
     {
-        Gia_ManEquivImprove( pAig );
+//        Gia_ManEquivImprove( pAig );
         pNew = Gia_ManCorrReduce( pAig );
         pNew = Gia_ManSeqCleanup( pTemp = pNew );
         Gia_ManStop( pTemp );
@@ -947,6 +1054,8 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
             100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
     }
+    if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
+        printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
     return pNew;
 }
 
diff --git a/src/aig/cec/cecCorr_updated.c b/src/aig/cec/cecCorr_updated.c
new file mode 100644
index 00000000..dbe81d81
--- /dev/null
+++ b/src/aig/cec/cecCorr_updated.c
@@ -0,0 +1,1022 @@
+/**CFile****************************************************************
+
+  FileName    [cecCorr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinational equivalence checking.]
+
+  Synopsis    [Latch/signal correspondence computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the real value of the literal w/o spec reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
+{
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
+        return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
+    }
+    if ( f == 0 )
+    {
+        assert( Gia_ObjIsRo(p, pObj) );
+        return Gia_ObjCopyF(p, f, pObj);
+    }
+    assert( f && Gia_ObjIsRo(p, pObj) );
+    pObj = Gia_ObjRoToRi( p, pObj );
+    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
+    return Gia_ObjFanin0CopyF( p, f-1, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively performs speculative reduction for the object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
+{
+    Gia_Obj_t * pRepr;
+    int iLitNew;
+    if ( ~Gia_ObjCopyF(p, f, pObj) )
+        return;
+    if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
+        iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+        Gia_ObjSetCopyF( p, f, pObj, iLitNew );
+        return;
+    }
+    assert( Gia_ObjIsCand(pObj) );
+    iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
+    Gia_ObjSetCopyF( p, f, pObj, iLitNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives SRM for signal correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    Vec_Int_t * vXorLits;
+    int f, i, iPrev, iObj, iPrevNew, iObjNew;
+    assert( nFrames > 0 );
+    assert( Gia_ManRegNum(p) > 0 );
+    assert( p->pReprs != NULL );
+    p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+            Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
+    for ( f = 0; f < nFrames+fScorr; f++ )
+    { 
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+    }
+    *pvOutputs = Vec_IntAlloc( 1000 );
+    vXorLits = Vec_IntAlloc( 1000 );
+    if ( fRings )
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            if ( Gia_ObjIsConst( p, i ) )
+            {
+                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
+                iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
+                if ( iObjNew != 0 )
+                {
+                    Vec_IntPush( *pvOutputs, 0 );
+                    Vec_IntPush( *pvOutputs, i );
+                    Vec_IntPush( vXorLits, iObjNew );
+                }
+            }
+            else if ( Gia_ObjIsHead( p, i ) )
+            {
+                iPrev = i;
+                Gia_ClassForEachObj1( p, i, iObj )
+                {
+                    iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                    iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
+                    iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
+                    iObjNew  = Gia_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
+                    if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
+                    {
+                        Vec_IntPush( *pvOutputs, iPrev );
+                        Vec_IntPush( *pvOutputs, iObj );
+                        Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
+                    }
+                    iPrev = iObj;
+                }
+                iObj = i;
+                iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
+                iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
+                iObjNew  = Gia_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
+                if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
+                {
+                    Vec_IntPush( *pvOutputs, iPrev );
+                    Vec_IntPush( *pvOutputs, iObj );
+                    Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
+                }
+            }
+        }
+    }
+    else
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+            if ( pRepr == NULL )
+                continue;
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
+            iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+            if ( iPrevNew != iObjNew )
+            {
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+            }
+        }
+    }
+    Vec_IntForEachEntry( vXorLits, iObjNew, i )
+        Gia_ManAppendCo( pNew, iObjNew );
+    Vec_IntFree( vXorLits );
+    Gia_ManHashStop( pNew );
+    ABC_FREE( p->pCopies );
+//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives SRM for signal correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    Vec_Int_t * vXorLits;
+    int f, i, iPrevNew, iObjNew;
+    assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
+    assert( Gia_ManRegNum(p) > 0 );
+    assert( p->pReprs != NULL );
+    p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        Gia_ManAppendCi(pNew);
+        Gia_ObjSetCopyF( p, 0, pObj, 0 );
+    }
+    for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
+    { 
+        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
+        Gia_ManForEachPi( p, pObj, i )
+            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
+    }
+    *pvOutputs = Vec_IntAlloc( 1000 );
+    vXorLits = Vec_IntAlloc( 1000 );
+    for ( f = nPrefix; f < nFrames+nPrefix; f++ )
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+            if ( pRepr == NULL )
+                continue;
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
+            iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+            if ( iPrevNew != iObjNew )
+            {
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
+                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
+                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
+            }
+        }
+    }
+    Vec_IntForEachEntry( vXorLits, iObjNew, i )
+        Gia_ManAppendCo( pNew, iObjNew );
+    Vec_IntFree( vXorLits );
+    Gia_ManHashStop( pNew );
+    ABC_FREE( p->pCopies );
+//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes simulation info for lcorr/scorr counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops, int * pInitState )
+{
+    unsigned * pInfo;
+    int k, w, nWords;
+    nWords = Vec_PtrReadWordsSimInfo( vInfo );
+    assert( nFlops <= Vec_PtrSize(vInfo) );
+    for ( k = 0; k < nFlops; k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        if ( pInitState && Gia_InfoHasBit(pInitState, k) )
+        {
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = ~0;
+//            pInfo[0] <<= 1;
+        }
+        else
+        {
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = 0;
+        }
+    }
+    for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Gia_ManRandom( 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps simulation info from SRM to the original AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
+{
+    Gia_Obj_t * pObj, * pRepr;
+    unsigned * pInfoObj, * pInfoRepr;
+    int i, w, nWords;
+    nWords = Vec_PtrReadWordsSimInfo( vInfo );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        // skip ROs without representatives
+        pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+        if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
+            continue;
+        pInfoObj = Vec_PtrEntry( vInfo, i );
+        for ( w = 0; w < nWords; w++ )
+            assert( pInfoObj[w] == 0 );
+        // skip ROs with constant representatives
+        if ( Gia_ObjIsConst0(pRepr) )
+            continue;
+        assert( Gia_ObjIsRo(p, pRepr) );
+//        printf( "%d -> %d    ", i, Gia_ObjId(p, pRepr) );
+        // transfer info from the representative
+        pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
+        for ( w = 0; w < nWords; w++ )
+            pInfoObj[w] = pInfoRepr[w];
+    }
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects information about remapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
+{
+    Vec_Int_t * vPairs;
+    Gia_Obj_t * pObj, * pRepr;
+    int i;
+    vPairs = Vec_IntAlloc( 100 );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        // skip ROs without representatives
+        pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
+//        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
+            continue;
+        assert( Gia_ObjIsRo(p, pRepr) );
+//        printf( "%d -> %d    ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
+        // remember the pair
+        Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
+        Vec_IntPush( vPairs, i );
+    }
+    return vPairs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps simulation info from SRM to the original AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo, int * pInitState )
+{
+    unsigned * pInfoObj, * pInfoRepr;
+    int w, i, iObj, iRepr, nWords;
+    nWords = Vec_PtrReadWordsSimInfo( vInfo );
+    Vec_IntForEachEntry( vPairs, iRepr, i )
+    {
+        iObj = Vec_IntEntry( vPairs, ++i );
+        pInfoObj = Vec_PtrEntry( vInfo, iObj );
+        pInfoRepr = Vec_PtrEntry( vInfo, iRepr );
+        for ( w = 0; w < nWords; w++ )
+        {
+            assert( pInitState || pInfoObj[w] == 0 );
+            pInfoObj[w] = pInfoRepr[w];
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Packs one counter-examples into the array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+*************************************`**********************************/
+int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
+{
+    unsigned * pInfo, * pPres;
+    int i;
+    for ( i = 0; i < nLits; i++ )
+    {
+        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+        if ( Gia_InfoHasBit( pPres, iBit ) && 
+             Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+             return 0;
+    }
+    for ( i = 0; i < nLits; i++ )
+    {
+        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+        Gia_InfoSetBit( pPres, iBit );
+        if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+            Gia_InfoXorBit( pInfo, iBit );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs bitpacking of counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
+{ 
+    Vec_Int_t * vPat;
+    Vec_Ptr_t * vPres;
+    int nWords = Vec_PtrReadWordsSimInfo(vInfo);
+    int nBits = 32 * nWords; 
+    int k, nSize, iBit = 1, kMax = 0;
+    vPat  = Vec_IntAlloc( 100 );
+    vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
+    Vec_PtrCleanSimInfo( vPres, 0, nWords );
+    while ( iStart < Vec_IntSize(vCexStore) )
+    {
+        // skip the output number
+        iStart++;
+        // get the number of items
+        nSize = Vec_IntEntry( vCexStore, iStart++ );
+        if ( nSize <= 0 )
+            continue;
+        // extract pattern
+        Vec_IntClear( vPat );
+        for ( k = 0; k < nSize; k++ )
+            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
+        // add pattern to storage
+        for ( k = 1; k < nBits; k++ )
+            if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+                break;
+        kMax = ABC_MAX( kMax, k );
+        if ( k == nBits-1 )
+            break;
+    }
+    Vec_PtrFree( vPres );
+    Vec_IntFree( vPat );
+    return iStart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs bitpacking of counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
+{ 
+    unsigned * pInfo;
+    int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo); 
+    int k, iLit, nLits, Out, iBit = 1;
+    while ( iStart < Vec_IntSize(vCexStore) )
+    {
+        // skip the output number
+//        iStart++;
+        Out = Vec_IntEntry( vCexStore, iStart++ );
+//        printf( "iBit = %d. Out = %d.\n", iBit, Out );
+        // get the number of items
+        nLits = Vec_IntEntry( vCexStore, iStart++ );
+        if ( nLits <= 0 )
+            continue;
+        // add pattern to storage
+        for ( k = 0; k < nLits; k++ )
+        {
+            iLit = Vec_IntEntry( vCexStore, iStart++ );
+            pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
+            if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
+                Gia_InfoXorBit( pInfo, iBit );
+        }
+        if ( ++iBit == nBits )
+            break;
+    }
+//    printf( "added %d bits\n", iBit-1 );
+    return iStart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates counter-examples derived by the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, int * pInitState )
+{ 
+    Vec_Int_t * vPairs;
+    Vec_Ptr_t * vSimInfo; 
+    int RetValue = 0, iStart = 0;
+    vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
+    Gia_ManSetRefs( pSim->pAig );
+//    pSim->pPars->nWords  = 63;
+    pSim->pPars->nRounds = nFrames;
+    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
+    while ( iStart < Vec_IntSize(vCexStore) )
+    {
+        Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig), pInitState );
+        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
+//        iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
+//        Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
+        Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState );
+        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
+//        Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
+    }
+//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
+    assert( iStart == Vec_IntSize(vCexStore) );
+    Vec_PtrFree( vSimInfo );
+    Vec_IntFree( vPairs );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates counter-examples derived by the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore )
+{ 
+    Vec_Ptr_t * vSimInfo; 
+    int RetValue = 0, iStart = 0;
+    Gia_ManSetRefs( pSim->pAig );
+    pSim->pPars->nRounds = 1;
+    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
+    while ( iStart < Vec_IntSize(vCexStore) )
+    {
+        Cec_ManStartSimInfo( vSimInfo, 0, NULL );
+        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
+        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
+    }
+    assert( iStart == Vec_IntSize(vCexStore) );
+    Vec_PtrFree( vSimInfo );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates equivalence classes by marking those that timed out.]
+
+  Description [Returns 1 if all ndoes are proved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
+{
+    int i, status, iRepr, iObj;
+    int Counter = 0;
+    assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
+    Vec_StrForEachEntry( vStatus, status, i )
+    {
+        iRepr = Vec_IntEntry( vOutputs, 2*i );
+        iObj  = Vec_IntEntry( vOutputs, 2*i+1 );
+        if ( status == 1 )
+            continue;
+        if ( status == 0 )
+        {
+            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
+                Counter++;
+//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
+//                printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
+//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
+//                Cec_ManSimClassRemoveOne( pSim, iObj );
+            continue;
+        }
+        if ( status == -1 )
+        {
+//            if ( !Gia_ObjFailed( p, iObj ) )
+//                printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
+//            Gia_ObjSetFailed( p, iRepr );
+//            Gia_ObjSetFailed( p, iObj );        
+//            if ( fRings )
+//            Cec_ManSimClassRemoveOne( pSim, iRepr );
+            Cec_ManSimClassRemoveOne( pSim, iObj );
+            continue;
+        }
+    }
+//    if ( Counter )
+//    printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        Gia_ManCorrReduce_rec( pNew, p, pRepr );
+        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        return;
+    }
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces AIG using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics during solving.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
+{ 
+    int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
+    int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( Gia_ObjIsNone(p, i) )
+            CounterX++;
+        else if ( Gia_ObjIsConst(p, i) )
+            Counter0++;
+        else if ( Gia_ObjIsHead(p, i) )
+            Counter++;
+    }
+    CounterX -= Gia_ManCoNum(p);
+    nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+    if ( iIter == -1 )
+        printf( "BMC : " );
+    else
+        printf( "%3d : ", iIter );
+    printf( "c =%8d  cl =%7d  lit =%8d  ", Counter0, Counter, nLits );
+    if ( vStatus )
+    Vec_StrForEachEntry( vStatus, Entry, i )
+    {
+        if ( Entry == 1 )
+            nProve++;
+        else if ( Entry == 0 )
+            nDispr++;
+        else if ( Entry == -1 )
+            nFail++;
+    }
+    printf( "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
+    ABC_PRT( "T", Time );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes new initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
+{  
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    unsigned * pInitState;
+    int i, f; 
+    printf( "Simulating %d timeframes.\n", nFrames );
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark1 = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManConst0(pAig)->fMark1 = 0;
+        Gia_ManForEachPi( pAig, pObj, i )
+            pObj->fMark1 = Gia_ManRandom(0) & 1;
+//            pObj->fMark1 = 1;
+        Gia_ManForEachAnd( pAig, pObj, i )
+            pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & 
+                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachRi( pAig, pObj, i )
+            pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
+            pObjRo->fMark1 = pObjRi->fMark1;
+    }
+    pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) );
+    Gia_ManForEachRo( pAig, pObj, i )
+    {
+        if ( pObj->fMark1 )
+            Gia_InfoSetBit( pInitState, i );
+//        printf( "%d", pObj->fMark1 );
+    }
+//    printf( "\n" );
+    Gia_ManCleanMark1( pAig );
+    return pInitState;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Internal procedure for register correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
+{  
+    int nIterMax = 100000;
+    int nAddFrames = 1; // additional timeframes to simulate
+    Vec_Str_t * vStatus;
+    Vec_Int_t * vOutputs;
+    Vec_Int_t * vCexStore;
+    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+    Cec_ManSim_t * pSim;
+    Gia_Man_t * pSrm;
+    unsigned * pInitState = NULL;
+    int r, RetValue, clkTotal = clock();
+    int clkSat = 0, clkSim = 0, clkSrm = 0;
+    int clk2, clk = clock();
+    ABC_FREE( pAig->pReprs );
+    ABC_FREE( pAig->pNexts );
+    if ( Gia_ManRegNum(pAig) == 0 )
+    {
+        printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
+        return 0;
+    }
+    Gia_ManRandom( 1 );
+    // derive initial state for resimulation
+    if ( pPars->nPrefix )
+//        pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) );
+        pInitState = Cec_ManComputeInitState( pAig, 100 );
+    // prepare simulation manager
+    Cec_ManSimSetDefaultParams( pParsSim );
+    pParsSim->nWords     = pPars->nWords;
+    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->fVerbose   = pPars->fVerbose;
+    pParsSim->fLatchCorr = pPars->fLatchCorr;
+    pParsSim->fSeqSimulate = 1;
+    // create equivalence classes of registers
+    pSim = Cec_ManSimStart( pAig, pParsSim, pInitState );
+    Cec_ManSimClassesPrepare( pSim );
+    Cec_ManSimClassesRefine( pSim );
+    // prepare SAT solving
+    Cec_ManSatSetDefaultParams( pParsSat );
+    pParsSat->nBTLimit = pPars->nBTLimit;
+    pParsSat->fVerbose = pPars->fVerbose;
+    if ( pPars->fVerbose )
+    {
+        printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
+            Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), 
+            pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
+        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
+    }
+    // perform refinement of equivalence classes
+    for ( r = 0; r < nIterMax; r++ )
+    { 
+        clk = clock();
+        // perform speculative reduction
+        clk2 = clock();
+        pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
+        clkSrm += clock() - clk2;
+        if ( Gia_ManCoNum(pSrm) == 0 )
+        {
+            Vec_IntFree( vOutputs );
+            Gia_ManStop( pSrm );            
+            break;
+        }
+//Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
+        // found counter-examples to speculation
+        clk2 = clock();
+        if ( pPars->fUseCSat )
+            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+        else
+            vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+        Gia_ManStop( pSrm );
+        clkSat += clock() - clk2;
+        if ( Vec_IntSize(vCexStore) == 0 )
+        {
+            Vec_IntFree( vCexStore );
+            Vec_StrFree( vStatus );
+            Vec_IntFree( vOutputs );
+            break;
+        }
+        // refine classes with these counter-examples
+        clk2 = clock();
+        RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState );
+        Vec_IntFree( vCexStore );
+        clkSim += clock() - clk2;
+        Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+        if ( pPars->fVerbose )
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+        Vec_StrFree( vStatus );
+        Vec_IntFree( vOutputs );
+//Gia_ManEquivPrintClasses( pAig, 1, 0 );
+    }
+    ABC_FREE( pInitState );
+    // check the base case
+    if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix )
+    {
+        int fChanges = 1;
+        while ( fChanges )
+        {
+            int clkBmc = clock();
+            fChanges = 0;
+            pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+            if ( Gia_ManPoNum(pSrm) == 0 )
+            {
+                Gia_ManStop( pSrm );
+                Vec_IntFree( vOutputs );
+                break;
+            }
+            pParsSat->nBTLimit *= 10;
+            if ( pPars->nPrefix )
+            {
+                pParsSat->nBTLimit = 10000;
+                vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+            }
+            else if ( pPars->fUseCSat )
+                vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+            else
+                vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+            // refine classes with these counter-examples
+            if ( Vec_IntSize(vCexStore) )
+            {
+                clk2 = clock();
+                RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames + pPars->nPrefix, NULL );
+                clkSim += clock() - clk2;
+                Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+                fChanges = 1;
+            }
+            if ( pPars->fVerbose )
+                Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+            // recycle
+            Vec_IntFree( vCexStore );
+            Vec_StrFree( vStatus );
+            Gia_ManStop( pSrm );
+            Vec_IntFree( vOutputs );
+        }
+    }
+    else
+    {
+        if ( pPars->fVerbose )
+            Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
+    }
+    // check the overflow
+    if ( r == nIterMax )
+        printf( "The refinement was not finished. The result may be incorrect.\n" );
+    Cec_ManSimStop( pSim );
+    clkTotal = clock() - clkTotal;
+    // report the results
+    if ( pPars->fVerbose )
+    {
+        ABC_PRTP( "Srm  ", clkSrm,                        clkTotal );
+        ABC_PRTP( "Sat  ", clkSat,                        clkTotal );
+        ABC_PRTP( "Sim  ", clkSim,                        clkTotal );
+        ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
+        ABC_PRT( "TOTAL",  clkTotal );
+    }
+    return 0;
+}    
+
+/**Function*************************************************************
+
+  Synopsis    [Top-level procedure for register correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
+{  
+    Gia_Man_t * pNew, * pTemp;
+    int RetValue;
+    RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
+    // derive reduced AIG
+    if ( pPars->fMakeChoices )
+    {
+        pNew = Gia_ManEquivToChoices( pAig, 1 );
+        Gia_ManHasChoices( pNew );
+    }
+    else
+    {
+        Gia_ManEquivImprove( pAig );
+        pNew = Gia_ManCorrReduce( pAig );
+        pNew = Gia_ManSeqCleanup( pTemp = pNew );
+        Gia_ManStop( pTemp );
+        //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
+    }
+    // report the results
+    if ( pPars->fVerbose )
+    {
+        printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
+            Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 
+            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
+            Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
+            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
+    }
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 5f032b59..3a8d8588 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -823,13 +823,13 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
         {
             if ( Gia_ObjFaninC0(pObj) )
             {
-                printf( "Constant 1 output of SRM!!!\n" );
+//                printf( "Constant 1 output of SRM!!!\n" );
                 Cec_ManSatAddToStore( vCexStore, p->vCex, i ); // trivial counter-example
                 Vec_StrPush( vStatus, 0 );
             }
             else
             {
-                printf( "Constant 0 output of SRM!!!\n" );
+//                printf( "Constant 0 output of SRM!!!\n" );
                 Vec_StrPush( vStatus, 1 );
             }
             continue;
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index 1e1e4edb..7f7b1b4c 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -627,6 +627,7 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot )
 {
     Aig_Obj_t * pObj;
     int i;
+    Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL );
     Vec_PtrForEachEntry( p->vCutNodes, pObj, i )
         if ( !Aig_ObjIsNone(pObj) )
             Dar_ObjSetCuts( pObj, NULL );
@@ -653,7 +654,7 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
     Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
     Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
     Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
-    int i, k, RetValue;
+    int i, k, RetValue; 
 
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index 7b23aa33..7f9188e0 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -813,6 +813,12 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
             pData->Level = Aig_Regular(pData->pFunc)->Level;
             // mark the node if it is part of MFFC
             pData->fMffc = Aig_ObjIsTravIdCurrent(p->pAig, Aig_Regular(pData->pFunc));
+            // assign the probability
+            if ( p->pPars->fPower )
+            {
+                float Prob = Aig_Int2Float( Vec_IntEntry( p->pAig->vProbs, Aig_ObjId(Aig_Regular(pData->pFunc)) ) );
+                pData->dProb = Aig_IsComplement(pData->pFunc)? 1.0-Prob : Prob;
+            }
         }
     }
 }
@@ -830,22 +836,30 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class, Aig_Obj_t * pRoot )
 ***********************************************************************/
 int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required, float * pPower )
 {
-    float Power0, Power1;
     Dar_LibDat_t * pData;
+    float Power0, Power1;
     int Area;
     if ( pPower )
         *pPower = (float)0.0;
+    pData = s_DarLib->pDatas + pObj->Num;
+    if ( pData->TravId == Out )
+        return 0;
+    pData->TravId = Out;
     if ( pObj->fTerm )
+    {
+        if ( pPower )
+            *pPower = pData->dProb;
         return 0;
+    }
     assert( pObj->Num > 3 );
-    pData = s_DarLib->pDatas + pObj->Num;
     if ( pData->Level > Required )
         return 0xff;
     if ( pData->pFunc && !pData->fMffc )
+    {
+        if ( pPower )
+            *pPower = pData->dProb;
         return 0;
-    if ( pData->TravId == Out )
-        return 0;
-    pData->TravId = Out;
+    }
     // this is a new node - get a bound on the area of its branches
     nNodesSaved--;
     Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1, pPower? &Power0 : NULL );
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2d633d5c..571a6ef8 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -513,6 +513,7 @@ extern Gia_Man_t *         Gia_ManDupOrderDfs( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
 
+extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
 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_ManDupFlopClass( Gia_Man_t * p, int iClass );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index a4f1ab44..4b3692e4 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -105,6 +105,46 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Gia_ManStart( Aig_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsAnd(pObj) )
+            pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+        else if ( Aig_ObjIsPi(pObj) )
+            pObj->iData = Gia_ManAppendCi( pNew );
+        else if ( Aig_ObjIsPo(pObj) )
+            pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->iData = 1;
+        else
+            assert( 0 );
+    }
+    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    if ( pNew->pNexts )
+        Gia_ManDeriveReprs( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Handles choices as additional combinational outputs.]
 
   Description []
@@ -243,6 +283,43 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
     return pMan;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers representatives from pGia to pAig.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia )
+{
+    Aig_Obj_t * pObj;
+    Gia_Obj_t * pGiaObj, * pGiaRepr;
+    int i;
+    assert( p->pReprs == NULL );
+    assert( pGia->pReprs != NULL );
+    // move pointers from AIG to GIA
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        assert( i == 0 || !Gia_LitIsCompl(pObj->iData) );
+        pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) );
+        pGiaObj->Value = i;
+    }
+    // set the pointers to the nodes in AIG
+    Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
+    Gia_ManForEachObj( pGia, pGiaObj, i )
+    {
+        pGiaRepr = Gia_ObjReprObj( pGia, i );
+        if ( pGiaRepr == NULL )
+            continue;
+        Aig_ObjCreateRepr( p, Aig_ManObj(p, pGiaRepr->Value), Aig_ManObj(p, pGiaObj->Value) );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 0c0ee598..507e5143 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -47,8 +47,10 @@
 
 /*=== giaAig.c =============================================================*/
 extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t *         Gia_ManFromAigSimple( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
 extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
+extern void                Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index f53a3d33..e005dfc2 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -473,6 +473,8 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
     Vec_IntShrink( p->vLevReas, 3*iBound );
 }
 
+int s_Counter = 0;
+
 /**Function*************************************************************
 
   Synopsis    [Assigns the variables a value.]
@@ -498,6 +500,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi
     Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
     Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
     assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
+    s_Counter++;
 }
 
 
@@ -925,6 +928,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
 int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
 {
     int RetValue = 0;
+    s_Counter = 0;
     assert( !p->pProp.iHead && !p->pProp.iTail );
     assert( !p->pJust.iHead && !p->pJust.iTail );
     assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
@@ -941,6 +945,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
     p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Cbs_ManCheckLimits( p ) )
         RetValue = -1;
+
+//    printf( "%d ", s_Counter );
     return RetValue;
 }
 
@@ -1019,7 +1025,7 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
         {
             if ( Gia_ObjFaninC0(pRoot) )
             {
-                printf( "Constant 1 output of SRM!!!\n" );
+//                printf( "Constant 1 output of SRM!!!\n" );
                 Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
                 Vec_StrPush( vStatus, 0 );
             }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 63748403..cde19a22 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -246,6 +246,47 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while complementing the flops.]
+
+  Description [The array of initial state contains the init state
+  for each state bit of the flops in the design.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            pObj->Value = Gia_ManAppendCi( pNew );
+            if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) )
+                pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+            if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) )
+                pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit(pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
+            pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
+        }
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
 
 
 /**Function*************************************************************
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 0a44d2dc..c8d38331 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -162,9 +162,10 @@ struct Ntl_Net_t_
         int            iTemp;          // other data
     };
     Ntl_Obj_t *        pDriver;        // driver of the net
-    int                NetId;          // unique ID of the net
-    char               nVisits;        // the number of times the net is visited
-    char               fMark;          // temporary mark
+    unsigned           NetId     : 28; // unique ID of the net
+    unsigned           nVisits   :  2; // the number of times the net is visted
+    unsigned           fMark     :  1; // temporary mark
+    unsigned           fFixed    :  1; // the fixed net
     char               pName[0];       // the name of this net
 };
 
@@ -392,6 +393,7 @@ extern ABC_DLL int             Ntl_ModelSeqLeafNum( Ntl_Mod_t * p );
 extern ABC_DLL int             Ntl_ModelSeqRootNum( Ntl_Mod_t * p );
 extern ABC_DLL int             Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
 extern ABC_DLL void            Ntl_ModelClearNets( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ManRemoveUselessNets( Ntl_Man_t * p );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 405ec83f..70f97d89 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -422,6 +422,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
 
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
+//Ntl_ManPrintStats( p );
+//Aig_ManPrintStats( pAig );
     pNew = Ntl_ManInsertAig( p, pAig );
     pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
     if ( pAigCol == NULL )
@@ -429,6 +431,8 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
         Aig_ManStop( pAig );
         return pNew;
     }
+//Ntl_ManPrintStats( pNew );
+//Aig_ManPrintStats( pAigCol );
 
     // perform SCL for the given design
     pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 21f2d246..eb967bdc 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -245,6 +245,42 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
 
 /**Function*************************************************************
 
+  Synopsis    [Find drivers of the given net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetThis;
+    int i, k;
+    pRoot = Ntl_ManRootModel( p );
+    pNetThis = Ntl_ModelFindNet( pRoot, pName );
+    printf( "\n*** Net %d \"%s\":\n", pNetThis->NetId, pName );
+    // mark from the nodes
+    Ntl_ModelForEachPo( pRoot, pNode, i )
+        if ( pNetThis == Ntl_ObjFanin0(pNode) )
+            printf( "driven by PO %d\n", i );
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+        Ntl_ObjForEachFanin( pNode, pNet, k )
+            if ( pNetThis == pNet )
+                printf( "driven by node %d with %d fanins and %d fanouts\n (%s)\n", 
+                    pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName );
+    Ntl_ModelForEachBox( pRoot, pNode, i )
+        Ntl_ObjForEachFanin( pNode, pNet, k )
+            if ( pNetThis == pNet )
+                printf( "driven by box %d with %d fanins and %d fanouts\n (%s)\n", 
+                    pNode->Id, Ntl_ObjFaninNum(pNode), Ntl_ObjFanoutNum(pNode), Ntl_ObjFanout(pNode,0)->pName );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Inserts the given mapping into the netlist.]
 
   Description []
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 552d5c15..4c9bb311 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -460,6 +460,8 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
         }
         else
             pNet->pCopy = NULL;
+        if ( pNet->pCopy )
+            ((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed;
     }
     Ntl_ModelForEachObj( pModelOld, pObj, i )
     {
@@ -511,6 +513,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_ModelForEachNet( pModelOld, pNet, i )
     {
         pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        ((Ntl_Net_t *)pNet->pCopy)->fFixed = pNet->fFixed;
         if ( pNet->pDriver == NULL )
         {
             assert( !pModelOld->attrWhite );
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 9c3d4e42..6d1b6c83 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -657,6 +657,68 @@ void Ntl_ModelClearNets( Ntl_Mod_t * pModel )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Removes nets without fanins and fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManRemoveUselessNets( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet;
+    int i, k, Counter;
+    pRoot = Ntl_ManRootModel( p );
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+        pNet->fMark = 0;
+    Ntl_ModelForEachPi( pRoot, pNode, i )
+    {
+        pNet = Ntl_ObjFanout0(pNode);
+        pNet->fMark = 1;
+    }
+    Ntl_ModelForEachPo( pRoot, pNode, i )
+    {
+        pNet = Ntl_ObjFanin0(pNode);
+        pNet->fMark = 1;
+    }
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+    {
+        Ntl_ObjForEachFanin( pNode, pNet, k )
+            pNet->fMark = 1;
+        Ntl_ObjForEachFanout( pNode, pNet, k )
+            pNet->fMark = 1;
+    }
+    Ntl_ModelForEachBox( pRoot, pNode, i )
+    {
+        Ntl_ObjForEachFanin( pNode, pNet, k )
+            pNet->fMark = 1;
+        Ntl_ObjForEachFanout( pNode, pNet, k )
+            pNet->fMark = 1;
+    }
+    Counter = 0;
+    Ntl_ModelForEachNet( pRoot, pNet, i )
+    {
+        if ( pNet->fMark )
+        {
+            pNet->fMark = 0;
+            continue;
+        }
+        if ( pNet->fFixed )
+            continue;
+        Ntl_ModelDeleteNet( pRoot, pNet );
+        Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
+        Counter++;
+    }
+    if ( Counter )
+        printf( "Deleted %d nets without fanins/fanouts.\n", Counter );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 10b7b462..12a72e2f 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -518,9 +518,21 @@ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
     Vec_Int_t * vTruth;
     Nwk_Obj_t * pObj;
     int i, Counter = 0;
+    Nwk_Obj_t * pNodeThis = pNtk->vObjs->pArray[72688];
+
     vTruth = Vec_IntAlloc( 1 << 16 );
     Nwk_ManForEachNode( pNtk, pObj, i )
+    {
+        if ( i == 641386 )
+        {
+            int x = 0;
+        }
         Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose );
+        if ( pNodeThis->nFanouts != 15 )
+        {
+            int s = 0;
+        }
+    }
     if ( fVerbose && Counter )
         printf( "Support minimization reduced support of %d nodes.\n", Counter );
     Vec_IntFree( vTruth );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 5ddef829..c7109e26 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -90,7 +90,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 nFramesBmc, int nConfMaxBmc, int fVerbose );
+extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
 /*=== saigBmc.c ==========================================================*/
 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 );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index a2a915f7..f6845acd 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -765,7 +765,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
   SeeAlso     []
  
 ***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
 {
     Aig_Man_t * pResult, * pTemp;
     Cnf_Dat_t * pCnf;
@@ -869,9 +869,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
                 Aig_ManPrintStats( pResult );
             else
                 printf( " -----------------------------------------------------\n" );
+            if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
+            {
+                printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio );
+                break;
+            }
         }
     }
-
     Vec_IntFree( vFlops );
     return pResult;
 }
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index adb98401..c2a33ee4 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -61,6 +61,8 @@ struct Ssw_Pars_t_
     int              fLocalSim;     // enable local simulation simulation
     int              fPartSigCorr;  // uses partial signal correspondence
     int              nIsleDist;     // extends islands by the given distance
+    int              fScorrGia;     // new signal correspondence implementation
+    int              fUseCSat;      // new SAT solver using when fScorrGia is selected
     int              fVerbose;      // verbose stats
     int              fFlopVerbose;  // verbose printout of redundant flops
     // optimized latch correspondence
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 56b37fbe..41123ca4 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -277,6 +277,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
              || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
             return Ssw_SignalCorrespondencePart( pAig, pPars );
     }
+
+    if ( pPars->fScorrGia )
+    {
+        extern Aig_Man_t * Cec_SignalCorrespondence( Aig_Man_t * pAig, int nConfs, int fUseCSat );
+        return Cec_SignalCorrespondence( pAig, pPars->nBTLimit, pPars->fUseCSat );
+    }
+
     // start the induction manager
     p = Ssw_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 3e233d90..6973bb64 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1185,6 +1185,81 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches )
         fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Converts the network to sequential.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd )
+{
+    Abc_Obj_t * pObjLi, * pObjLo, * pObj;
+    int i;
+    assert( Abc_NtkBoxNum(pNtk) == 0 );
+    if ( !Abc_NtkIsComb(pNtk) )
+    {
+        printf( "The network is a not a combinational one.\n" );
+        return;
+    }
+    if ( nLatchesToAdd >= Abc_NtkPiNum(pNtk) )
+    {
+        printf( "The number of latches is more or equal than the number of PIs.\n" );
+        return;
+    }
+    if ( nLatchesToAdd >= Abc_NtkPoNum(pNtk) )
+    {
+        printf( "The number of latches is more or equal than the number of POs.\n" );
+        return;
+    }
+
+    // move the last PIs to become CIs
+    Vec_PtrClear( pNtk->vPis );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( i < Abc_NtkCiNum(pNtk) - nLatchesToAdd )
+        {
+            Vec_PtrPush( pNtk->vPis, pObj );
+            continue;
+        }
+        pObj->Type = ABC_OBJ_BO;
+        pNtk->nObjCounts[ABC_OBJ_PI]--;
+        pNtk->nObjCounts[ABC_OBJ_BO]++;
+    }
+
+    // move the last POs to become COs
+    Vec_PtrClear( pNtk->vPos );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        if ( i < Abc_NtkCoNum(pNtk) - nLatchesToAdd )
+        {
+            Vec_PtrPush( pNtk->vPos, pObj );
+            continue;
+        }
+        pObj->Type = ABC_OBJ_BI;
+        pNtk->nObjCounts[ABC_OBJ_PO]--;
+        pNtk->nObjCounts[ABC_OBJ_BI]++;
+    }
+
+    // create latches
+    for ( i = 0; i < nLatchesToAdd; i++ )
+    {
+        pObjLo = Abc_NtkCi( pNtk, Abc_NtkCiNum(pNtk) - nLatchesToAdd + i );
+        pObjLi = Abc_NtkCo( pNtk, Abc_NtkCoNum(pNtk) - nLatchesToAdd + i );
+        pObj = Abc_NtkCreateLatch( pNtk );
+        Abc_ObjAddFanin( pObj, pObjLi );
+        Abc_ObjAddFanin( pObjLo, pObj );
+        Abc_LatchSetInit0( pObj );
+    }
+
+    if ( !Abc_NtkCheck( pNtk ) )
+        fprintf( stdout, "Abc_NtkMakeSeq(): Network check has failed.\n" );
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6beaf144..f8815321 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -261,6 +261,7 @@ static int Abc_CommandAbc8Lutmin     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Balance    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Speedup    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Merge      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Insert     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc8Fraig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -578,6 +579,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*b",            Abc_CommandAbc8Balance,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*speedup",      Abc_CommandAbc8Speedup,      0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*merge",        Abc_CommandAbc8Merge,        0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*insert",       Abc_CommandAbc8Insert,       0 );
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*fraig",        Abc_CommandAbc8Fraig,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
@@ -5281,6 +5283,8 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int fRemoveLatches;
+    int nLatchesToAdd;
+    extern void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5288,11 +5292,23 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fRemoveLatches = 0;
+    nLatchesToAdd = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Llh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            } 
+            nLatchesToAdd = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLatchesToAdd < 0 ) 
+                goto usage;
+            break;
         case 'l':
             fRemoveLatches ^= 1;
             break;
@@ -5308,7 +5324,12 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsComb(pNtk) )
+    if ( Abc_NtkIsComb(pNtk) && nLatchesToAdd == 0 )
+    {
+        fprintf( pErr, "The network is already combinational.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsComb(pNtk) && nLatchesToAdd != 0 )
     {
         fprintf( pErr, "The network is already combinational.\n" );
         return 0;
@@ -5316,15 +5337,19 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     pNtkRes = Abc_NtkDup( pNtk );
-    Abc_NtkMakeComb( pNtkRes, fRemoveLatches );
+    if ( nLatchesToAdd ) 
+        Abc_NtkMakeSeq( pNtkRes, nLatchesToAdd );
+    else
+        Abc_NtkMakeComb( pNtkRes, fRemoveLatches );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: comb [-lh]\n" );
-    fprintf( pErr, "\t        makes the current network combinational by replacing latches by PI/PO pairs\n" );
-    fprintf( pErr, "\t-l    : toggle removing latches [default = %s]\n", fRemoveLatches? "yes": "no" );
+    fprintf( pErr, "usage: comb [-L num] [-lh]\n" );
+    fprintf( pErr, "\t        converts comb network into seq, and vice versa\n" );
+    fprintf( pErr, "\t-L    : number of latches to add to comb network (0 = do not add) [default = %d]\n", nLatchesToAdd );
+    fprintf( pErr, "\t-l    : toggle converting latches to PIs/POs or removing them [default = %s]\n", fRemoveLatches? "remove": "convert" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -8449,7 +8474,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 //    Abc_NtkDarTest( pNtk );
 
-    Bbl_ManTest( pNtk );
+//    Bbl_ManTest( pNtk );
+
+    {
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    extern void Aig_ManFactorAlgebraicTest( Aig_Man_t * p );
+    Aig_Man_t * pAig;
+    pAig = Abc_NtkToDar( pNtk, 0, 0 );
+    Aig_ManFactorAlgebraicTest( pAig );
+    Aig_ManStop( pAig );
+    }
+
 //    Bbl_ManSimpleDemo();
     return 0;
 usage:
@@ -9576,7 +9611,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pNtk == NULL )
+    if ( pNtk == NULL ) 
     {
         fprintf( pErr, "Empty network.\n" );
         return 1;
@@ -18480,9 +18515,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fSkipProof;
     int nFramesBmc;
     int nConfMaxBmc;
+    int nRatio;
     int fVerbose;
     int c;
-    extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -18496,9 +18532,10 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSkipProof  =     0;
     nFramesBmc  =  2000;
     nConfMaxBmc =  5000;
+    nRatio      =    10;
     fVerbose    =     0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDdesvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGDRdesvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18546,6 +18583,17 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfMaxBmc < 0 ) 
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRatio = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRatio < 0 ) 
+                goto usage;
+            break;
         case 'd':
             fDynamic ^= 1;
             break;
@@ -18579,9 +18627,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
+    if ( !(0 <= nRatio && nRatio <= 100) )
+    {
+        fprintf( stdout, "Wrong value of parameter \"-R <num>\".\n" );
+        return 0;
+    }
 
     // modify the current network
-    pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
+    pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose );
     if ( pNtkRes == NULL )
     {
         if ( pNtk->pSeqModel == NULL )
@@ -18592,13 +18645,14 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 usage:
-    fprintf( pErr, "usage: abs [-FCGD num] [-desvh]\n" );
+    fprintf( pErr, "usage: abs [-FCGDR num] [-desvh]\n" );
     fprintf( pErr, "\t         proof-based abstraction (PBA) using UNSAT core of BMC\n" );
     fprintf( pErr, "\t         followed by counter-example-based abstraction\n" );
     fprintf( pErr, "\t-F num : the max number of timeframes for PBA [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-G num : the max number of timeframes for BMC [default = %d]\n", nFramesBmc );
     fprintf( pErr, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", nConfMaxBmc );
+    fprintf( pErr, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", nRatio );
     fprintf( pErr, "\t-d     : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
     fprintf( pErr, "\t-e     : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
     fprintf( pErr, "\t-s     : toggle skipping proof-based abstraction [default = %s]\n", fSkipProof? "yes": "no" );
@@ -18806,7 +18860,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Ioa_WriteBlif( pTemp, "test_boxes.blif" );
         Ntl_ManFree( pTemp );
         }
-        return 0;
+        return 0; 
     }
 
     Abc_FrameClearDesign(); 
@@ -18960,7 +19014,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     fCollapsed = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "abch" ) ) != EOF )
-    {
+    { 
         switch ( c )
         {
         case 'a':
@@ -19392,7 +19446,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( pAbc->pAbc8Lib == NULL )
         {
-            printf( "LUT library is not given. Using default 6-LUT library.\n" );
+            printf( "LUT library is not given. Using default LUT library.\n" );
             pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
         }
         printf( "MAPPED:  " );
@@ -19480,7 +19534,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pAbc->pAbc8Lib == NULL )
     {
-        printf( "LUT library is not given. Using default 6-LUT library.\n" );
+        printf( "LUT library is not given. Using default LUT library.\n" );
         pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
     }
 
@@ -20460,8 +20514,6 @@ usage:
     return 1;
 }
 
-
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -20606,6 +20658,56 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8Insert( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
+    void * pNtlNew;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Insert(): There is no design.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Nwk == NULL ) 
+    {
+        printf( "Abc_CommandAbc8Insert(): There is no network to insert.\n" );
+        return 1;
+    }
+    pNtlNew = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *insert [-h]\n" );
+    fprintf( stdout, "\t         inserts the mapped network into the netlist\n" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     void * pNtlNew;
@@ -21148,7 +21250,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Ssw_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsncvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -21274,6 +21376,12 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fLocalSim ^= 1;
             break;
+        case 'n':
+            pPars->fScorrGia ^= 1;
+            break;
+        case 'c':
+            pPars->fUseCSat ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -21327,7 +21435,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsvh]\n" );
+    fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsncvh]\n" );
     fprintf( stdout, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
     fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -21343,6 +21451,8 @@ usage:
     fprintf( stdout, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
     fprintf( stdout, "\t-d     : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
     fprintf( stdout, "\t-s     : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" );
+    fprintf( stdout, "\t-n     : toggle using new AIG package [default = %s]\n", pPars->fScorrGia? "yes": "no" );
+    fprintf( stdout, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -21414,7 +21524,7 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_FrameClearDesign(); 
         pAbc->pAbc8Ntl = pNtlTemp;
     }
-
+ 
     // sweep the current design
     Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
     if ( Counter == 0 )
@@ -23389,7 +23499,7 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cec_ManCorSetDefaultParams( pPars );
     pPars->fLatchCorr = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23415,6 +23525,17 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPrefix = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPrefix < 0 ) 
+                goto usage;
+            break;
         case 'f':
             pPars->fFirstStop ^= 1;
             break;
@@ -23447,10 +23568,11 @@ int Abc_CommandAbc9Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &lcorr [-FC num] [-frcvh]\n" );
+    fprintf( stdout, "usage: &lcorr [-FCP num] [-frcvh]\n" );
     fprintf( stdout, "\t         performs latch correpondence computation\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
     fprintf( stdout, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
@@ -23477,7 +23599,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Cec_ManCorSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPfrecvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23503,6 +23625,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPrefix = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPrefix < 0 ) 
+                goto usage;
+            break;
         case 'f':
             pPars->fFirstStop ^= 1;
             break;
@@ -23538,10 +23671,11 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" );
+    fprintf( stdout, "usage: &scorr [-FCP num] [-frecvh]\n" );
     fprintf( stdout, "\t         performs signal correpondence computation\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
+    fprintf( stdout, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
     fprintf( stdout, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
     fprintf( stdout, "\t-e     : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
@@ -24297,7 +24431,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars );
     if ( pAbc->pAbc8Lib == NULL )
     {
-        printf( "LUT library is not given. Using default 6-LUT library.\n" );
+        printf( "LUT library is not given. Using default LUT library.\n" );
         pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
     }
     // set defaults
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a5973153..ab47d797 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1743,6 +1743,18 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
         RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
         // transfer model if given
 //        pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
+        if ( RetValue == 0  && (Abc_NtkLatchNum(pNtk) == 0) )
+        {
+            pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
+            printf( "Networks are not equivalent.\n" );
+            ABC_PRT( "Time", clock() - clk );
+            if ( pSecPar->fReportSolution )
+            {
+                printf( "SOLUTION: FAIL       " );
+                ABC_PRT( "Time", clock() - clkTotal );
+            }
+            return RetValue;
+        }
         Abc_NtkDelete( pNtkComb );
         // return the result, if solved
         if ( RetValue == 1 )
@@ -2570,7 +2582,7 @@ ABC_PRT( "Time", clock() - clkTotal );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
@@ -2580,7 +2592,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
         return NULL;
 
     Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, fVerbose );
+    pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fSkipProof, nFramesBmc, nConfMaxBmc, nRatio, fVerbose );
     if ( pTemp->pSeqModel )
     {
         ABC_FREE( pNtk->pModel );
@@ -2710,7 +2722,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation
     // consider the case of one output
     if ( Abc_NtkCoNum(pNtkOn) == 1 )
         return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
-    // start the new newtork
+    // start the new network
     pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
     Abc_NtkForEachPi( pNtkOn, pObj, i )
@@ -3393,7 +3405,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
         return NULL;
 /*
     Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 1 );
+    pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, 1 );
     Aig_ManStop( pTemp );
     if ( pMan == NULL )
         return NULL;
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 114288ba..bf082456 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -103,6 +103,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
     Abc_Ntk_t * pNtkAig;
     Abc_Obj_t * pObj;
     int i, nNodes;//, RetValue;
+    int Counter = 0;
     assert( Abc_NtkIsStrash(pNtk) );
 //timeRetime = clock();
     // print warning about choice nodes
@@ -112,8 +113,14 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // complement the 1-values registers
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        if ( Abc_LatchIsInit1(pObj) )
+    {
+        if ( Abc_LatchIsInitDc(pObj) )
+            Counter++;
+        else if ( Abc_LatchIsInit1(pObj) )
             Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
+    }
+    if ( Counter )
+    printf( "Converting %d flops from don't-care to zero initial value.\n", Counter );
     // restrash the nodes (assuming a topological order of the old network)
     Abc_NtkForEachNode( pNtk, pObj, i )
         pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 76a82b51..5e9093e7 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -204,6 +204,7 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe
     {
         Abc_NtkForEachPi( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, fUseXval? ABC_INIT_DC : Abc_XsimRand2() );
+//            Abc_ObjSetXsim( pObj, ABC_INIT_ONE );
         Abc_AigForEachAnd( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
         Abc_NtkForEachCo( pNtk, pObj, i )
@@ -213,7 +214,11 @@ void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fUseXval, int fVe
     }
     // set the final values
     Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
         pObj->pData = (void *)(ABC_PTRINT_T)Abc_ObjGetXsim(Abc_ObjFanout0(pObj));
+//        printf( "%d", Abc_LatchIsInit1(pObj) );
+    }
+//    printf( "\n" );
 }
 
 ///////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 46d61583..75419e0f 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1823,13 +1823,18 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     int c;
     int fNames;
+    int forceSeq;
 
     fNames = 0;
+    forceSeq = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "snh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 's':
+                forceSeq ^= 1;
+                break;
             case 'n':
                 fNames ^= 1;
                 break;
@@ -1912,8 +1917,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         }
         if ( fNames )
         {
+            char *cycle_ctr = forceSeq?"@0":"";
             Abc_NtkForEachPi( pNtk, pObj, i )
-                fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
+//                fprintf( pFile, "%s=%c\n", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
+                fprintf( pFile, "%s%s=%c\n", Abc_ObjName(pObj), cycle_ctr, '0'+(pNtk->pModel[i]==1) );
         }
         else
         {
@@ -1927,9 +1934,10 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_counter [-snh] <file>\n" );
     fprintf( pAbc->Err, "\t         saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
     fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
+    fprintf( pAbc->Err, "\t-s     : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
     fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );