Version abc90424

26 files changed, 1813 insertions, 88 deletions

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