Version abc90424

6 files changed, 1236 insertions, 75 deletions

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;