Version abc90329

11 files changed, 1236 insertions, 43 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index a97bd958..e26455ba 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -61,6 +61,7 @@ struct Cec_ParSim_t_
     int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
     int              fSeqSimulate;  // performs sequential simulation
+    int              fLatchCorr;    // consider only latch outputs
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
@@ -113,6 +114,36 @@ struct Cec_ParCec_t_
     int              fVerbose;      // verbose stats
 };
 
+// sequential register correspodence parameters
+typedef struct Cec_ParCor_t_ Cec_ParCor_t;
+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              nBTLimit;      // conflict limit at a node
+    int              fLatchCorr;    // consider only latch outputs
+    int              fUseRings;     // use rings
+    int              fUseCSat;      // use circuit-based solver
+    int              fFirstStop;    // stop on the first sat output
+    int              fUseSmartCnf;  // use smart CNF computation
+    int              fVeryVerbose;  // verbose stats
+    int              fVerbose;      // verbose stats
+};
+
+// sequential register correspodence parameters
+typedef struct Cec_ParChc_t_ Cec_ParChc_t;
+struct Cec_ParChc_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nRounds;       // the number of simulation rounds
+    int              nBTLimit;      // conflict limit at a node
+    int              fFirstStop;    // stop on the first sat output
+    int              fUseSmartCnf;  // use smart CNF computation
+    int              fVeryVerbose;  // verbose stats
+    int              fVerbose;      // verbose stats
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -124,12 +155,18 @@ struct Cec_ParCec_t_
 /*=== cecCec.c ==========================================================*/
 extern int           Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
 extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
+/*=== cecChoice.c ==========================================================*/
+extern Gia_Man_t *   Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
+/*=== cecCorr.c ==========================================================*/
+extern Gia_Man_t *   Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
 /*=== cecCore.c ==========================================================*/
 extern void          Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
 extern void          Cec_ManSimSetDefaultParams( Cec_ParSim_t * p );
 extern void          Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p );
 extern void          Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
 extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
+extern void          Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
+extern void          Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
 extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
 extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern void          Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
new file mode 100644
index 00000000..ff30e1bb
--- /dev/null
+++ b/src/aig/cec/cecChoice.c
@@ -0,0 +1,51 @@
+/**CFile****************************************************************
+
+  FileName    [cecChoice.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Computation of structural choices.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
+{
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 26ff543a..a8ed017a 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -293,6 +293,48 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
 
 /**Function*************************************************************
 
+  Synopsis    [Refines one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i )
+{
+    int iRepr, Ent;
+    if ( Gia_ObjIsConst(p->pAig, i) )
+    {
+        Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+        return 1;
+    }
+    if ( !Gia_ObjIsClass(p->pAig, i) )
+        return 0;
+    assert( Gia_ObjIsClass(p->pAig, i) );
+    iRepr = Gia_ObjRepr( p->pAig, i );
+    if ( iRepr == GIA_VOID )
+        iRepr = i;
+    // collect nodes
+    Vec_IntClear( p->vClassOld );
+    Vec_IntClear( p->vClassNew );
+    Gia_ClassForEachObj( p->pAig, iRepr, Ent )
+    {
+        if ( Ent == i )
+            Vec_IntPush( p->vClassNew, Ent );
+        else
+            Vec_IntPush( p->vClassOld, Ent );
+    }
+    assert( Vec_IntSize( p->vClassNew ) == 1 );
+    Cec_ManSimClassCreate( p->pAig, p->vClassOld );
+    Cec_ManSimClassCreate( p->pAig, p->vClassNew );
+    assert( !Gia_ObjIsClass(p->pAig, i) );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes hash key of the simuation info.]
 
   Description []
@@ -797,8 +839,12 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
     p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
     p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
     // set starting representative of internal nodes to be constant 0
-    Gia_ManForEachObj( p->pAig, pObj, i )
-        Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
+    if ( p->pPars->fLatchCorr )
+        Gia_ManForEachObj( p->pAig, pObj, i )
+            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+    else
+        Gia_ManForEachObj( p->pAig, pObj, i )
+            Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
     // if sequential simulation, set starting representative of ROs to be constant 0
     if ( p->pPars->fSeqSimulate )
         Gia_ManForEachRo( p->pAig, pObj, i )
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 9274dcb8..d3c54948 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -156,6 +156,56 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParCor_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->nFrames        =       1;  // the number of time frames
+    p->nBTLimit       =     100;  // conflict limit at a node
+    p->fLatchCorr     =       0;  // consider only latch outputs
+    p->fUseRings      =       1;  // combine classes into rings
+    p->fUseCSat       =       1;  // use circuit-based solver
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+}  
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParChc_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+}  
+
+/**Function*************************************************************
+
   Synopsis    [Core procedure for SAT sweeping.]
 
   Description []
@@ -171,7 +221,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
     Cec_ManPat_t * pPat;
     pPat = Cec_ManPatStart();
     Cec_ManSatSolve( pPat, pAig, pPars );
-    pNew = Gia_ManDupDfsSkip( pAig );
+//    pNew = Gia_ManDupDfsSkip( pAig );
+    pNew = Gia_ManDup( pAig );
     Cec_ManPatStop( pPat );
     return pNew;
 }
@@ -193,7 +244,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
     int RetValue, clkTotal = clock();
     if ( pPars->fSeqSimulate )
         printf( "Performing sequential simulation of %d frames with %d words.\n", 
-            pPars->nWords, pPars->nRounds );
+            pPars->nRounds, pPars->nWords );
     Aig_ManRandom( 1 );
     pSim = Cec_ManSimStart( pAig, pPars );
     if ( pAig->pReprs == NULL )
@@ -286,7 +337,7 @@ p->timeSim += clock() - clk;
 //        Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
 
         if ( pPars->fVeryVerbose )
-            Gia_ManPrintStats( pSrm );
+            Gia_ManPrintStats( pSrm, 0 );
         if ( Gia_ManCoNum(pSrm) == 0 )
         {
             Gia_ManStop( pSrm );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
new file mode 100644
index 00000000..abc76416
--- /dev/null
+++ b/src/aig/cec/cecCorr.c
@@ -0,0 +1,757 @@
+/**CFile****************************************************************
+
+  FileName    [cecLcorr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Flop correspondence computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecLcorr.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 );
+
+////////////////////////////////////////////////////////////////////////
+///                     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 )
+{
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f );
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f );
+        return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
+    }
+    assert( f && Gia_ObjIsRo(p, pObj) );
+    pObj = Gia_ObjRoToRi( p, pObj );
+    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 );
+    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 )
+{
+    Gia_Obj_t * pRepr;
+    int iLitNew;
+    if ( ~Gia_ObjCopyF(p, f, pObj) )
+        return;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        if ( !Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
+        {
+            Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
+            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 );
+    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 = Aig_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))) )
+        {
+            if ( !Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), 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 ) )
+            {
+                if ( Gia_ObjIsFailedPair(p, 0, i) )
+                    continue;
+                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
+                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 )
+                {
+                    if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
+                    {
+                        iPrev = iObj;
+                        continue;
+                    }
+                    iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
+                    iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
+                    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;
+                if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
+                    continue;
+                iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
+                iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
+                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;
+            if ( Gia_ObjIsFailedPair(p, Gia_ObjRepr(p, i), i) )
+                continue;
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
+            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    [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    [Remaps simulation info from SRM to the original AIG.]
+
+  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 )
+{
+    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( pInfoObj[w] == 0 );
+            pInfoObj[w] = pInfoRepr[w];
+        }
+    }
+}
+
+/**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;
+    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) )
+//                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;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks all the nodes as proved.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSetProvedNodes( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, nLits = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjRepr(p, i) == GIA_VOID )
+            continue;
+        if ( Gia_ObjIsFailedPair( p, Gia_ObjRepr(p, i), i ) )
+            continue;
+        Gia_ObjSetProved( p, i );
+        nLits++;
+    }
+//    printf( "Identified %d proved literals.\n", nLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManLCorrPrintStats( 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;
+    printf( "%3d : c =%8d  cl =%7d  lit =%8d  ", iIter, 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    [Sets register values from the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
+{
+    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 );
+        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] = Aig_ManRandom( 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  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 ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
+                Aig_InfoXorBit( pInfo, iBit );
+        }
+        if ( ++iBit == nBits )
+            break;
+    }
+//    printf( "added %d bits\n", iBit-1 );
+    return iStart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Packs patterns into 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 ( Aig_InfoHasBit( pPres, iBit ) && 
+             Aig_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]));
+        Aig_InfoSetBit( pPres, iBit );
+        if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+            Aig_InfoXorBit( pInfo, iBit );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  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++ ) );
+//            printf( "%d(%d) ", Vec_IntEntryLast(vPat)/2, (Vec_IntEntryLast(vPat)&1)==0 );
+        }
+//        printf( "\n" );
+        // add pattern to storage
+        for ( k = 1; k < nBits; k++ )
+            if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+                break;
+//        for ( i = 0; i < 27; i++ )
+//            printf( "%d(%d) ", i, Aig_InfoHasBit(Vec_PtrEntry(vInfo,i), k) );
+//        printf( "\n" );
+
+        kMax = AIG_MAX( kMax, k );
+        if ( k == nBits-1 )
+            break;
+    }
+//        printf( "\n" );
+//    printf( "kMax = %d.\n", kMax );
+    Vec_PtrFree( vPres );
+    Vec_IntFree( vPat );
+    return iStart;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
+{ 
+    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) )
+    {
+//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
+        Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
+        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
+//        iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
+//        Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
+        Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
+        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    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
+{  
+    int nAddFrames = 2; // additional timeframes to simulate
+    Vec_Str_t * vStatus;
+    Vec_Int_t * vOutputs;
+    Vec_Int_t * vCexStore;
+    Gia_Man_t * pNew, * pTemp;
+    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+    Cec_ManSim_t * pSim;
+    Gia_Man_t * pSrm;
+    int r, RetValue;
+    int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
+    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 NULL;
+    }
+    Aig_ManRandom( 1 );
+    // 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 );
+    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_ManLCorrPrintStats( pAig, NULL, 0, clock() - clk );
+    }
+    // perform refinement of equivalence classes
+    for ( r = 0; r < 100000; 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_ManSolveMiter( pSrm, pPars->nBTLimit, &vStatus );
+        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 );
+        Vec_IntFree( vCexStore );
+        clkSim += clock() - clk2;
+        Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+        if ( pPars->fVerbose )
+            Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk );
+//Gia_ManEquivPrintClasses( pAig, 1, 0 );
+        Vec_StrFree( vStatus );
+        Vec_IntFree( vOutputs );
+    }
+    Cec_ManSimStop( pSim );
+    clkTotal = clock() - clkTotal;
+    if ( pPars->fVerbose )
+        Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
+    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 );
+    }
+    // derive reduced AIG
+    Gia_ManSetProvedNodes( pAig );
+    pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
+//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
+    pNew = Gia_ManSeqCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index ae4c6ff4..86af2614 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -85,15 +85,19 @@ struct Cec_ManSat_t_
     int              nRecycles;      // the number of times SAT solver was recycled
     int              nCallsSince;    // the number of calls since the last recycle
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
+    // counter-examples
+    Vec_Int_t *      vCex;           // the latest counter-example
+    Vec_Int_t *      vVisits;        // temporary array for visited nodes  
     // SAT calls statistics
     int              nSatUnsat;      // the number of proofs
     int              nSatSat;        // the number of failure
     int              nSatUndec;      // the number of timeouts
     int              nSatTotal;      // the number of calls
+    int              nCexLits;
     // conflicts
-    int              nConfUnsat;
-    int              nConfSat;
-    int              nConfUndec;
+    int              nConfUnsat;     // conflicts in unsat problems
+    int              nConfSat;       // conflicts in sat problems
+    int              nConfUndec;     // conflicts in undec problems
     // runtime stats
     int              timeSatUnsat;   // unsat
     int              timeSatSat;     // sat
@@ -164,6 +168,7 @@ struct Cec_ManFra_t_
 
 /*=== cecCore.c ============================================================*/
 /*=== cecClass.c ============================================================*/
+extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p );
 extern int                  Cec_ManSimClassesRefine( Cec_ManSim_t * p );
 extern int                  Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
@@ -183,10 +188,16 @@ extern void                 Cec_ManFraStop( Cec_ManFra_t * p );
 /*=== cecPat.c ============================================================*/
 extern void                 Cec_ManPatSavePattern( Cec_ManPat_t *  pPat, Cec_ManSat_t *  p, Gia_Obj_t * pObj );
 extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nWords );
+extern Vec_Ptr_t *          Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
+/*=== cecSeq.c ============================================================*/
+extern int                  Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
+extern int                  Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState );
+extern void                 Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
-extern void                 Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
+extern Vec_Str_t *          Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
+extern Vec_Int_t *          Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
 /*=== ceFraeep.c ============================================================*/
 extern Gia_Man_t *          Cec_ManFraSpecReduction( Cec_ManFra_t * p );
 extern int                  Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 14f2493e..430d961e 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -52,6 +52,8 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
     p->pSatVars     = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
     p->vUsedNodes   = Vec_PtrAlloc( 1000 );
     p->vFanins      = Vec_PtrAlloc( 100 );
+    p->vCex         = Vec_IntAlloc( 100 );
+    p->vVisits      = Vec_IntAlloc( 100 );
     return p;
 }
 
@@ -81,6 +83,7 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
     printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
         p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
     ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+    ABC_PRT( "Total time", p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -98,6 +101,8 @@ void Cec_ManSatStop( Cec_ManSat_t * p )
 {
     if ( p->pSat )
         sat_solver_delete( p->pSat );
+    Vec_IntFree( p->vCex );
+    Vec_IntFree( p->vVisits );
     Vec_PtrFree( p->vUsedNodes );
     Vec_PtrFree( p->vFanins );
     ABC_FREE( p->pSatVars );
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index b80f1e44..dacc5daf 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -450,7 +450,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     int nBits = 32 * nWords;
     int clk = clock();
     vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
-    Aig_ManRandomInfo( vInfo, 0, nWords );
+    Aig_ManRandomInfo( vInfo, 0, 0, nWords );
     vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
     Vec_PtrCleanSimInfo( vPres, 0, nWords );
     while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
@@ -464,7 +464,7 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
         if ( k == nBits-1 )
         {
             Vec_PtrReallocSimInfo( vInfo );
-            Aig_ManRandomInfo( vInfo, nWords, 2*nWords );
+            Aig_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
             Vec_PtrReallocSimInfo( vPres );
             Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
             nWords *= 2;
@@ -486,6 +486,77 @@ Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nW
     return vInfo;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Packs patterns into array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit )
+{
+    Vec_Int_t * vPat;
+    Vec_Ptr_t * vInfo, * vPres;
+    int k, nSize, iStart, kMax = 0, nPatterns = 0;
+    int nWords = nWordsInit;
+    int nBits = 32 * nWords;
+//    int RetValue;
+    assert( nRegs <= nInputs );
+    vPat  = Vec_IntAlloc( 100 );
+
+    vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
+    Vec_PtrCleanSimInfo( vInfo, 0, nWords );
+    Aig_ManRandomInfo( vInfo, nRegs, 0, nWords );
+
+    vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
+    Vec_PtrCleanSimInfo( vPres, 0, nWords );
+    iStart = 0;
+    while ( iStart < Vec_IntSize(vCexStore) )
+    {
+        nPatterns++;
+        // 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++, k += ((k % (32 * nWordsInit)) == 0) )
+            if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+                break;
+
+//        k = kMax + 1;
+//        RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
+//        assert( RetValue == 1 );
+
+        kMax = AIG_MAX( kMax, k );
+        if ( k == nBits-1 )
+        {
+            Vec_PtrReallocSimInfo( vInfo );
+            Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
+            Aig_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
+
+            Vec_PtrReallocSimInfo( vPres );
+            Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
+            nWords *= 2;
+            nBits *= 2;
+        }
+    }
+//    printf( "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
+    Vec_PtrFree( vPres );
+    Vec_IntFree( vPat );
+    return vInfo;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 1a398e2e..e69b526e 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -42,23 +42,32 @@
 void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
 {
     unsigned * pInfo;
-    int k, w, nWords;
+    int k, i, w, nWords;
     assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
-    assert( pCex->nBits <= Vec_PtrSize(vInfo) );
+    assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
     nWords = Vec_PtrReadWordsSimInfo( vInfo );
+/*
     for ( k = 0; k < pCex->nRegs; k++ )
     {
         pInfo = Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
             pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
     }
-    for ( ; k < pCex->nBits; k++ )
+*/
+    for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
     {
         pInfo = Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
+            pInfo[w] = 0;
+    }
+
+    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k++ );
+        for ( w = 0; w < nWords; w++ )
             pInfo[w] = Aig_ManRandom(0);
         // set simulation pattern and make sure it is second (first will be erased during simulation)
-        pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, k ); 
+        pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, i ); 
         pInfo[0] <<= 1;
     }
     for ( ; k < Vec_PtrSize(vInfo); k++ )
@@ -85,13 +94,13 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
     unsigned * pInfo;
     int k, w, nWords;
     nWords = Vec_PtrReadWordsSimInfo( vInfo );
-    assert( Gia_ManRegNum(pAig) == pCex->nRegs );
+    assert( pCex == NULL || Gia_ManRegNum(pAig) == pCex->nRegs );
     assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
     for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
     {
         pInfo = Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
-            pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+            pInfo[w] = (pCex && Aig_InfoHasBit(pCex->pData, k))? ~0 : 0;
     }
 
     for ( ; k < Vec_PtrSize(vInfo); k++ )
@@ -212,9 +221,10 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
         printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
         return -1;
     }
-    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
+//    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
+    if ( Gia_ManPiNum(pAig) != pCex->nPis )
     {
-        printf( "Cec_ManSeqResimulateCounter(): Parameters of the ccounter-example differ.\n" );
+        printf( "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
         return -1;
     }
     if ( pPars->fVerbose )
@@ -251,6 +261,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
     int nAddFrames = 10; // additional timeframes to simulate
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Vec_Ptr_t * vSimInfo; 
+    Vec_Str_t * vStatus;
     Gia_Cex_t * pState;
     Gia_Man_t * pSrm;
     int r, nPats, RetValue = -1;
@@ -284,13 +295,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
 //        Gia_ManPrintCounterExample( pState );
         // derive speculatively reduced model
         pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
-        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManPiNum(pAig) * pPars->nFrames );
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * pPars->nFrames) );
         // allocate room for simulation info
         vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
             Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
         Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
         // fill in simulation info with counter-examples
-        Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
+        vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
+        Vec_StrFree( vStatus );
         Gia_ManStop( pSrm );
         // resimulate and refine the classes
         RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 24d5c3ed..a69d1d2a 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -556,18 +556,10 @@ p->timeSatUndec += clock() - clk;
 ***********************************************************************/
 void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 {
-    static int Counter;
-//    char Buffer[1000];
-
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int i, status, clk = clock(), clk2;
-
-//    sprintf( Buffer, "gia%03d.aig", Counter++ );
-//Gia_WriteAiger( pAig, Buffer, 0, 0 );
-//printf( "Dumpted slice into file \"%s\".\n", Buffer );
-
     // reset the manager
     if ( pPat )
     {
@@ -595,13 +587,6 @@ clk2 = clock();
         pObj->fMark0 = (status == 0);
         pObj->fMark1 = (status == 1);
 /*
-printf( "Output %6d : ", i );
-printf( "conf = %6d ", p->pSat->stats.conflicts );
-printf( "prop = %6d ", p->pSat->stats.propagations );
-ABC_PRT( "time", clock() - clk2 );
-*/
-
-/*
         if ( status == -1 )
         {
             Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
@@ -653,6 +638,8 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
         unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
         if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
             Aig_InfoXorBit( pInfo, iPat );
+        pSat->nCexLits++;
+//        Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
         return;
     }
     assert( Gia_ObjIsAnd(pObj) );
@@ -672,44 +659,207 @@ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pOb
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
+Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
 {
     Bar_Progress_t * pProgress = NULL;
+    Vec_Str_t * vStatus;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int iPat = 1, nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
+    int iPat = 0, nPatsInit, nPats;
     int i, status, clk = clock();
+    nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
     Gia_ManResetTravId( pAig );
     p = Cec_ManSatCreate( pAig, pPars );
+    vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
     pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
     Gia_ManForEachCo( pAig, pObj, i )
     {
+        Bar_ProgressUpdate( pProgress, i, "SAT..." );
         if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+        {
+            if ( Gia_ObjFaninC0(pObj) )
+            {
+                printf( "Constant 1 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 0 );
+            }
+            else
+            {
+                printf( "Constant 0 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 1 );
+            }
             continue;
-        Bar_ProgressUpdate( pProgress, i, "BMC..." );
+        }
         status = Cec_ManSatCheckNode( p, pObj );
+//printf( "output %d   status = %d\n", i, status );
+        Vec_StrPush( vStatus, (char)status );
         if ( status != 0 )
             continue;
+        // resize storage
+        if ( iPat == nPats )
+        {
+            int nWords = Vec_PtrReadWordsSimInfo(vPatts);
+            Vec_PtrReallocSimInfo( vPatts );
+            Vec_PtrCleanSimInfo( vPatts, nWords, 2*nWords );
+            nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
+        }
+        if ( iPat % nPatsInit == 0 )
+            iPat++;
         // save the pattern
         Gia_ManIncrementTravId( pAig );
+//        Vec_IntClear( p->vCex );
         Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
-        if ( iPat == nPats )
-            break;
+//        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
+//        Cec_ManSatAddToStore( p->vCexStore, p->vCex );
+//        if ( iPat == nPats )
+//            break;
         // quit if one of them is solved
-        if ( pPars->fFirstStop )
-            break;
+//        if ( pPars->fFirstStop )
+//            break;
+//        if ( iPat == 32 * 15 * 16 - 1 )
+//            break;
     }
     p->timeTotal = clock() - clk;
     Bar_ProgressStop( pProgress );
     if ( pPars->fVerbose )
         Cec_ManSatPrintStats( p );
+//    printf( "Total number of cex literals = %d. (Ave = %d)\n", p->nCexLits, p->nCexLits/p->nSatSat );
     Cec_ManSatStop( p );
     if ( pnPats )
         *pnPats = iPat-1;
+    return vStatus;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Save values in the cone of influence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
+{
+    int i, Entry;
+    Vec_IntPush( vCexStore, Out );
+    if ( vCex == NULL ) // timeout
+    {
+        Vec_IntPush( vCexStore, -1 );
+        return;
+    }
+    // write the counter-example
+    Vec_IntPush( vCexStore, Vec_IntSize(vCex) );
+    Vec_IntForEachEntry( vCex, Entry, i )
+        Vec_IntPush( vCexStore, Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Save values in the cone of influence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        pSat->nCexLits++;
+        Vec_IntPush( pSat->vCex, Gia_Var2Lit( Gia_ObjCioId(pObj), !Cec_ObjSatVarValue(pSat, pObj) ) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin0(pObj) );
+    Cec_ManSatSolveMiter_rec( pSat, p, Gia_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of solving for the POs of the AIG.]
+
+  Description [Labels the nodes that have been proved (pObj->fMark1) 
+  and returns the set of satisfying assignments.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Vec_Int_t * vCexStore;
+    Vec_Str_t * vStatus;
+    Cec_ManSat_t * p;
+    Gia_Obj_t * pObj;
+    int i, status, clk = clock();
+    // prepare AIG
+    Gia_ManSetPhase( pAig );
+    Gia_ManLevelNum( pAig );
+    Gia_ManResetTravId( pAig );
+    // create resulting data-structures
+    vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+    vCexStore = Vec_IntAlloc( 10000 );
+    // perform solving
+    p = Cec_ManSatCreate( pAig, pPars );
+    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+    Gia_ManForEachCo( pAig, pObj, i )
+    {
+        Vec_IntClear( p->vCex );
+        Bar_ProgressUpdate( pProgress, i, "SAT..." );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+        {
+            if ( Gia_ObjFaninC0(pObj) )
+            {
+                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" );
+                Vec_StrPush( vStatus, 1 );
+            }
+            continue;
+        }
+        status = Cec_ManSatCheckNode( p, pObj );
+        Vec_StrPush( vStatus, (char)status );
+        if ( status == -1 )
+        {
+            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+            continue;
+        }
+        if ( status == 1 )
+            continue;
+        assert( status == 0 );
+        // save the pattern
+        Gia_ManIncrementTravId( pAig );
+        Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
+//        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
+        Cec_ManSatAddToStore( vCexStore, p->vCex, i );
+    }
+    p->timeTotal = clock() - clk;
+    Bar_ProgressStop( pProgress );
+//    if ( pPars->fVerbose )
+//        Cec_ManSatPrintStats( p );
+    Cec_ManSatStop( p );
+    *pvStatus = vStatus;
+    return vCexStore;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make
index 1fc9861c..35a18cae 100644
--- a/src/aig/cec/module.make
+++ b/src/aig/cec/module.make
@@ -1,6 +1,8 @@
 SRC +=    src/aig/cec/cecCec.c \
+    src/aig/cec/cecChoice.c \
     src/aig/cec/cecClass.c \
     src/aig/cec/cecCore.c \
+    src/aig/cec/cecCorr.c \
     src/aig/cec/cecIso.c \
     src/aig/cec/cecMan.c \
     src/aig/cec/cecPat.c \