Version abc70828

19 files changed, 1606 insertions, 460 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1ee62ad6..a6428e65 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -128,6 +128,8 @@ struct Aig_Man_t_
     int              fCatchExor;     // enables EXOR nodes
     int              fAddStrash;     // performs additional strashing
     Aig_Obj_t **     pObjCopies;     // mapping of AIG nodes into FRAIG nodes
+    void (*pImpFunc) (void*, void*); // implication checking precedure
+    void *           pImpData;       // implication checking data
     // timing statistics
     int              time1;
     int              time2;
@@ -298,6 +300,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 // iterator over the primary outputs
 #define Aig_ManForEachPo( p, pObj, i )                                          \
     Vec_PtrForEachEntry( p->vPos, pObj, i )
+// iterator over the assertions
+#define Aig_ManForEachAssert( p, pObj, i )                                      \
+    Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
 // iterator over all objects, including those currently not used
 #define Aig_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
@@ -373,15 +378,12 @@ extern void            Aig_ManFanoutStop( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
+extern Aig_Obj_t *     Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
 extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
-extern Aig_Man_t *     Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
-extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
-extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
-extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
@@ -436,6 +438,11 @@ extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern void            Aig_ManCreateChoices( Aig_Man_t * p );
 /*=== aigRet.c ========================================================*/
 extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
+/*=== aigScl.c ==========================================================*/
+extern Aig_Man_t *     Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap );
+extern int             Aig_ManSeqCleanup( Aig_Man_t * p );
+extern int             Aig_ManCountMergeRegs( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose );
 /*=== aigSeq.c ========================================================*/
 extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
 /*=== aigShow.c ========================================================*/
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 122daaa4..076cc420 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -172,54 +172,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
 
 /**Function*************************************************************
 
-  Synopsis    [Remaps the manager.]
-
-  Description [Map in the array specifies for each CI nodes the node that
-  should be used after remapping.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjMapped;
-    int i;
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
-    pNew->nRegs = p->nRegs;
-    pNew->nAsserts = p->nAsserts;
-    // create the PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pNew);
-    // implement the mapping
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        pObjMapped = Vec_PtrEntry( vMap, i );
-        pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
-    }
-    // duplicate internal nodes
-    Aig_ManForEachObj( p, pObj, i )
-        if ( Aig_ObjIsBuf(pObj) )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        else if ( Aig_ObjIsNode(pObj) )
-            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // add the POs
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-    assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
-    // check the resulting network
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Extracts the miter composed of XOR of the two nodes.]
 
   Description []
@@ -306,110 +258,6 @@ void Aig_ManStop( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    // collect latch input corresponding to unmarked PI (latch output)
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        Vec_PtrPush( vNodes, pObj->pNext );
-        return;
-    }
-    if ( Aig_ObjIsPo(pObj) )
-    {
-        Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
-        return;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of dangling nodes removed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManSeqCleanup( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes, * vCis, * vCos;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, nTruePis, nTruePos;
-    assert( Aig_ManBufNum(p) == 0 );
-
-    // mark the PIs
-    Aig_ManIncrementTravId( p );
-    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPiSeq( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
-
-    // prepare to collect nodes reachable from POs
-    vNodes = Vec_PtrAlloc( 100 );
-    Aig_ManForEachPoSeq( p, pObj, i )
-        Vec_PtrPush( vNodes, pObj );
-
-    // remember latch inputs in latch outputs
-    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-        pObjLo->pNext = pObjLi;
-    // mark the nodes reachable from these nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Aig_ManSeqCleanup_rec( p, pObj, vNodes );
-    assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
-    // clean latch output pointers
-    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-        pObjLo->pNext = NULL;
-
-    // if some latches are removed, update PIs/POs
-    if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
-    {
-        // collect new CIs/COs
-        vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
-        Aig_ManForEachPi( p, pObj, i )
-            if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-                Vec_PtrPush( vCis, pObj );
-        vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
-        Aig_ManForEachPo( p, pObj, i )
-            if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-                Vec_PtrPush( vCos, pObj );
-            else
-                Aig_ObjDisconnect( p, pObj );
-        // remember the number of true PIs/POs
-        nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
-        nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
-        // set the new number of registers
-        p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
-        // create new PIs/POs
-        assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
-        assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
-        Vec_PtrFree( p->vPis );    p->vPis = vCis;
-        Vec_PtrFree( p->vPos );    p->vPos = vCos;
-        p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
-        p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
-    }
-    Vec_PtrFree( vNodes );
-    // remove dangling nodes
-    return Aig_ManCleanup( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of dangling nodes removed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Aig_ManCleanup( Aig_Man_t * p )
 {
     Vec_Ptr_t * vObjs;
@@ -430,42 +278,6 @@ int Aig_ManCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of dangling nodes removed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManCountMergeRegs( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pFanin;
-    int i, Counter = 0, Const0 = 0, Const1 = 0;
-    Aig_ManIncrementTravId( p );
-    Aig_ManForEachLiSeq( p, pObj, i )
-    {
-        pFanin = Aig_ObjFanin0(pObj);
-        if ( Aig_ObjIsConst1(pFanin) )
-        {
-            if ( Aig_ObjFaninC0(pObj) )
-                Const0++;
-            else
-                Const1++;
-        }
-        if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
-            continue;
-        Aig_ObjSetTravIdCurrent(p, pFanin);
-        Counter++;
-    }
-    printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", 
-        Aig_ManRegNum(p), Counter, Const0, Const1 );
-    return 0;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -491,149 +303,6 @@ void Aig_ManPrintStats( Aig_Man_t * p )
     printf( "\n" );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Checks how many latches can be reduced.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManReduceLachesCount( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pFanin;
-    int i, Counter = 0;
-    assert( Aig_ManRegNum(p) > 0 );
-    Aig_ManForEachObj( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    Aig_ManForEachLiSeq( p, pObj, i )
-    {
-        pFanin = Aig_ObjFanin0(pObj);
-        if ( Aig_ObjFaninC0(pObj) )
-        {
-            if ( pFanin->fMarkB )
-                Counter++;
-            else
-                pFanin->fMarkB = 1;
-        }
-        else
-        {
-            if ( pFanin->fMarkA )
-                Counter++;
-            else
-                pFanin->fMarkA = 1;
-        }
-    }
-    Aig_ManForEachLiSeq( p, pObj, i )
-    {
-        pFanin = Aig_ObjFanin0(pObj);
-        pFanin->fMarkA = pFanin->fMarkB = 0;
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reduces the latches.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vMap;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
-    int * pMapping, i;
-    // start mapping by adding the true PIs
-    vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
-    Aig_ManForEachPiSeq( p, pObj, i )
-        Vec_PtrPush( vMap, pObj );
-    // create mapping of fanin nodes into the corresponding latch outputs
-    pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
-    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-    {
-        pFanin = Aig_ObjFanin0(pObjLi);
-        if ( Aig_ObjFaninC0(pObjLi) )
-        {
-            if ( pFanin->fMarkB )
-            {
-                Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
-            }
-            else
-            {
-                pFanin->fMarkB = 1;
-                pMapping[2*pFanin->Id + 1] = i;
-                Vec_PtrPush( vMap, pObjLo );
-            }
-        }
-        else
-        {
-            if ( pFanin->fMarkA )
-            {
-                Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
-            }
-            else
-            {
-                pFanin->fMarkA = 1;
-                pMapping[2*pFanin->Id] = i;
-                Vec_PtrPush( vMap, pObjLo );
-            }
-        }
-    }
-    free( pMapping );
-    Aig_ManForEachLiSeq( p, pObj, i )
-    {
-        pFanin = Aig_ObjFanin0(pObj);
-        pFanin->fMarkA = pFanin->fMarkB = 0;
-    }
-    return vMap;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reduces the latches.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
-{
-    Aig_Man_t * pTemp;
-    Vec_Ptr_t * vMap;
-    int nSaved, nCur;
-    for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur )
-    {
-        if ( fVerbose )
-        {
-        printf( "Saved = %5d.   ", nCur );
-        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
-        }
-        vMap = Aig_ManReduceLachesOnce( p );
-        p = Aig_ManRemap( pTemp = p, vMap );
-        Aig_ManStop( pTemp );
-        Vec_PtrFree( vMap );
-        Aig_ManSeqCleanup( p );
-        if ( fVerbose )
-        {
-        printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
-        printf( "\n" );
-        }
-    }
-    return p;
-}
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index f616bc25..d230f0d9 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -321,7 +321,7 @@ Vec_Vec_t * Aig_ManSupports( Aig_Man_t * pMan )
         }
         assert( 0 );
     }
-printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
+//printf( "Memory usage = %d Mb.\n", Vec_PtrSize(p->vMemory) * p->nChunkSize / (1<<20) );
     Part_ManStop( p );
     // sort supports by size
     Vec_VecSort( vSupps, 1 );
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 3e588979..cea3c438 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -253,7 +253,7 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb
 ***********************************************************************/
 Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
 {
-    int fOrdered = 1;
+    int fOrdered = 0;
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
new file mode 100644
index 00000000..f8989446
--- /dev/null
+++ b/src/aig/aig/aigScl.c
@@ -0,0 +1,370 @@
+/**CFile****************************************************************
+
+  FileName    [aigScl.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Sequential cleanup.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigScl.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps the manager.]
+
+  Description [Map in the array specifies for each CI nodes the node that
+  should be used after remapping.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjMapped;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // implement the mapping
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObjMapped = Vec_PtrEntry( vMap, i );
+        pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
+    }
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        else if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDup(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSeqCleanup_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    // collect latch input corresponding to unmarked PI (latch output)
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_PtrPush( vNodes, pObj->pNext );
+        return;
+    }
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ManSeqCleanup_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Aig_ManSeqCleanup_rec( p, Aig_ObjFanin1(pObj), vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSeqCleanup( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes, * vCis, * vCos;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, nTruePis, nTruePos;
+    assert( Aig_ManBufNum(p) == 0 );
+
+    // mark the PIs
+    Aig_ManIncrementTravId( p );
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+
+    // prepare to collect nodes reachable from POs
+    vNodes = Vec_PtrAlloc( 100 );
+    Aig_ManForEachPoSeq( p, pObj, i )
+        Vec_PtrPush( vNodes, pObj );
+
+    // remember latch inputs in latch outputs
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = pObjLi;
+    // mark the nodes reachable from these nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Aig_ManSeqCleanup_rec( p, pObj, vNodes );
+    assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
+    // clean latch output pointers
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        pObjLo->pNext = NULL;
+
+    // if some latches are removed, update PIs/POs
+    if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) )
+    {
+        // collect new CIs/COs
+        vCis = Vec_PtrAlloc( Aig_ManPiNum(p) );
+        Aig_ManForEachPi( p, pObj, i )
+            if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+                Vec_PtrPush( vCis, pObj );
+        vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
+        Aig_ManForEachPo( p, pObj, i )
+            if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+                Vec_PtrPush( vCos, pObj );
+            else
+                Aig_ObjDisconnect( p, pObj );
+        // remember the number of true PIs/POs
+        nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+        nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
+        // set the new number of registers
+        p->nRegs -= Aig_ManPoNum(p) - Vec_PtrSize(vNodes);
+        // create new PIs/POs
+        assert( Vec_PtrSize(vCis) == nTruePis + p->nRegs );
+        assert( Vec_PtrSize(vCos) == nTruePos + p->nRegs );
+        Vec_PtrFree( p->vPis );    p->vPis = vCis;
+        Vec_PtrFree( p->vPos );    p->vPos = vCos;
+        p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis );
+        p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+    }
+    Vec_PtrFree( vNodes );
+    // remove dangling nodes
+    return Aig_ManCleanup( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCountMergeRegs( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Counter = 0, Const0 = 0, Const1 = 0;
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjIsConst1(pFanin) )
+        {
+            if ( Aig_ObjFaninC0(pObj) )
+                Const0++;
+            else
+                Const1++;
+        }
+        if ( Aig_ObjIsTravIdCurrent(p, pFanin) )
+            continue;
+        Aig_ObjSetTravIdCurrent(p, pFanin);
+        Counter++;
+    }
+    printf( "Regs = %d. Fanins = %d. Const0 = %d. Const1 = %d.\n", 
+        Aig_ManRegNum(p), Counter, Const0, Const1 );
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks how many latches can be reduced.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManReduceLachesCount( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Counter = 0, Diffs = 0;
+    assert( Aig_ManRegNum(p) > 0 );
+    Aig_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjFaninC0(pObj) )
+        {
+            if ( pFanin->fMarkB )
+                Counter++;
+            else
+                pFanin->fMarkB = 1;
+        }
+        else
+        {
+            if ( pFanin->fMarkA )
+                Counter++;
+            else
+                pFanin->fMarkA = 1;
+        }
+    }
+    // count fanins that have both attributes
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        Diffs += pFanin->fMarkA && pFanin->fMarkB;
+        pFanin->fMarkA = pFanin->fMarkB = 0;
+    }
+//    printf( "Diffs = %d.\n", Diffs );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMap;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pFanin;
+    int * pMapping, i;
+    // start mapping by adding the true PIs
+    vMap = Vec_PtrAlloc( Aig_ManPiNum(p) );
+    Aig_ManForEachPiSeq( p, pObj, i )
+        Vec_PtrPush( vMap, pObj );
+    // create mapping of fanin nodes into the corresponding latch outputs
+    pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) );
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+    {
+        pFanin = Aig_ObjFanin0(pObjLi);
+        if ( Aig_ObjFaninC0(pObjLi) )
+        {
+            if ( pFanin->fMarkB )
+            {
+                Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id + 1]) );
+            }
+            else
+            {
+                pFanin->fMarkB = 1;
+                pMapping[2*pFanin->Id + 1] = i;
+                Vec_PtrPush( vMap, pObjLo );
+            }
+        }
+        else
+        {
+            if ( pFanin->fMarkA )
+            {
+                Vec_PtrPush( vMap, Aig_ManLo(p, pMapping[2*pFanin->Id]) );
+            }
+            else
+            {
+                pFanin->fMarkA = 1;
+                pMapping[2*pFanin->Id] = i;
+                Vec_PtrPush( vMap, pObjLo );
+            }
+        }
+    }
+    free( pMapping );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        pFanin->fMarkA = pFanin->fMarkB = 0;
+    }
+    return vMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Man_t * pTemp;
+    Vec_Ptr_t * vMap;
+    int nSaved, nCur;
+    for ( nSaved = 0; nCur = Aig_ManReduceLachesCount(p); nSaved += nCur )
+    {
+        if ( fVerbose )
+        {
+        printf( "Saved = %5d.   ", nCur );
+        printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+        }
+        vMap = Aig_ManReduceLachesOnce( p );
+        p = Aig_ManRemap( pTemp = p, vMap );
+        Aig_ManStop( pTemp );
+        Vec_PtrFree( vMap );
+        Aig_ManSeqCleanup( p );
+        if ( fVerbose )
+        {
+        printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
+        printf( "\n" );
+        }
+    }
+    return p;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index b8296cb2..e5b96879 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define TSI_MAX_ROUNDS    10000
+#define TSI_MAX_ROUNDS    1000
 
 #define AIG_XVS0   1
 #define AIG_XVS1   2
@@ -340,7 +340,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     }
     if ( f == TSI_MAX_ROUNDS )
     {
-        printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations.\n", TSI_MAX_ROUNDS );
+        printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
         Aig_TsiStop( pTsi );
         return NULL;
     }
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index cdf1fdf7..4d99e254 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -662,7 +662,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
 {
     FILE * pFile;
     Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj, * pConst1 = NULL;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL;
     int i, nDigits, Counter = 0;
     if ( Aig_ManPoNum(p) == 0 )
     {
@@ -687,14 +687,22 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     fprintf( pFile, ".model test\n" );
     // write PIs
     fprintf( pFile, ".inputs" );
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachPiSeq( p, pObj, i )
         fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
     fprintf( pFile, "\n" );
     // write POs
     fprintf( pFile, ".outputs" );
-    Aig_ManForEachPo( p, pObj, i )
+    Aig_ManForEachPoSeq( p, pObj, i )
         fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
     fprintf( pFile, "\n" );
+    // write latches
+    if ( Aig_ManRegNum(p) )
+    {
+    fprintf( pFile, "\n" );
+    Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+        fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData );
+    fprintf( pFile, "\n" );
+    }
     // write nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 45ed62ee..d1b1cd3b 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -9,6 +9,8 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigOrder.c \
     src/aig/aig/aigPart.c \
     src/aig/aig/aigRepr.c \
+    src/aig/aig/aigRet.c \
+    src/aig/aig/aigScl.c \
     src/aig/aig/aigSeq.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 217d1fba..931e0930 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -77,6 +77,7 @@ struct Fra_Par_t_
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
     int              fUseImps;          // use implications
+    int              fWriteImps;        // record implications
 };
 
 // FRAIG equivalence classes
@@ -148,7 +149,6 @@ struct Fra_Man_t_
     // statistics
     int              nSimRounds;
     int              nNodesMiter;
-    int              nLitsZero;
     int              nLitsBeg;
     int              nLitsEnd;
     int              nNodesBeg;
@@ -202,6 +202,10 @@ static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pN
 static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
 
+static inline int          Fra_ImpLeft( int Imp )                                        { return Imp & 0xFFFF;         }
+static inline int          Fra_ImpRight( int Imp )                                       { return Imp >> 16;            }
+static inline int          Fra_ImpCreate( int Left, int Right )                          { return (Right << 16) | Left; }
+
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -222,7 +226,7 @@ extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFai
 extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
 extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
-extern int                 Fra_ClassesRefine1( Fra_Cla_t * p );
+extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
 extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
 extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
 extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
@@ -233,18 +237,24 @@ extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
+extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
+extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
+extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
 /*=== fraImp.c ========================================================*/
 extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
 extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
 extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
+extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
+extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
+extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
+/*=== fraLcr.c ========================================================*/
+extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -259,7 +269,7 @@ extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, A
 extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
-extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
+extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 45c162af..648d08c4 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -31,6 +31,8 @@ struct Fra_Bmc_t_
     int              nPref;             // the size of the prefix
     int              nDepth;            // the depth of the frames
     int              nFramesAll;        // the total number of timeframes
+    // implications to be filtered
+    Vec_Int_t *      vImps;
     // AIG managers
     Aig_Man_t *      pAig;              // the original AIG manager
     Aig_Man_t *      pAigFrames;        // initialized timeframes
@@ -67,7 +69,6 @@ static inline Aig_Obj_t *  Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { asse
 int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
     Fra_Man_t * p = pObj0->pData;
-//    Aig_Obj_t ** ppNodes = p->pBmc->pObjToFraig;
     Aig_Obj_t * pObjFrames0, * pObjFrames1;
     Aig_Obj_t * pObjFraig0, * pObjFraig1;
     int i;
@@ -102,6 +103,69 @@ int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
     return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Refines implications using BMC.]
+
+  Description [The input is the combinational FRAIG manager,
+  which is used to FRAIG the timeframes. ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
+{
+    Aig_Obj_t * pLeft, * pRight;
+    Aig_Obj_t * pLeftT, * pRightT;
+    Aig_Obj_t * pLeftF, * pRightF;
+    int i, f, Imp, Left, Right;
+    int fComplL, fComplR;
+    assert( p->nFramesAll == 1 );
+    assert( p->pManAig == pBmc->pAigFrames );
+    Vec_IntForEachEntry( pBmc->vImps, Imp, i )
+    {
+        if ( Imp == 0 )
+            continue;
+        Left = Fra_ImpLeft(Imp);
+        Right = Fra_ImpRight(Imp);
+        // get the corresponding nodes
+        pLeft  = Aig_ManObj( pBmc->pAig, Left );
+        pRight = Aig_ManObj( pBmc->pAig, Right );
+        // iterate through the timeframes
+        for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
+        {
+            // get timeframes nodes
+            pLeftT  = Bmc_ObjFrames( pLeft, f );
+            pRightT = Bmc_ObjFrames( pRight, f );
+            // get the corresponding FRAIG nodes
+            pLeftF  = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
+            pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
+            // get the complemented attributes
+            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
+            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
+            // check equality
+            if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
+            {
+                if ( fComplL != fComplR )
+                    Vec_IntWriteEntry( pBmc->vImps, i, 0 );
+                break;
+            }
+            // check the implication 
+            // - if true, a clause is added
+            // - if false, a cex is simulated
+            // make sure the implication is refined
+            if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
+            {
+                Vec_IntWriteEntry( pBmc->vImps, i, 0 );
+                break;
+            }
+        }
+    }
+    Fra_ImpCompactArray( pBmc->vImps );
+}
+
 
 /**Function*************************************************************
 
@@ -125,8 +189,6 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
     p->nFramesAll = nPref + nDepth;
     p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
     memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
-//    p->pObjToFraig  = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
-//    memset( p->pObjToFraig, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
     return p;
 }
 
@@ -215,34 +277,6 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Constructs FRAIG manager for the initialized timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
-{
-    Aig_Man_t * pFraig;
-    Fra_Par_t Pars, * pPars = &Pars; 
-    Fra_ParamsDefault( pPars );
-    pPars->nBTLimitNode = 100000;
-    pPars->fVerbose     = 0;
-    pPars->fProve       = 0;
-    pPars->fDoSparse    = 1;
-    pPars->fSpeculate   = 0;
-    pPars->fChoicing    = 0;
-    pFraig = Fra_FraigPerform( p->pAigFrames, pPars );
-    p->pObjToFraig = p->pAigFrames->pObjCopies;
-    p->pAigFrames->pObjCopies = NULL;
-    return pFraig;
-} 
-
-/**Function*************************************************************
-
   Synopsis    [Performs BMC for the given AIG.]
 
   Description []
@@ -255,12 +289,22 @@ Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
 void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
 {
     Aig_Obj_t * pObj;
-    int i, clk = clock();
+    int i, nImpsOld, clk = clock();
     assert( p->pBmc == NULL );
     // derive and fraig the frames
     p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
     p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
-    p->pBmc->pAigFraig = Fra_BmcFraig( p->pBmc );
+    // if implications are present, configure the AIG manager to check them
+    if ( p->pCla->vImps )
+    {
+        p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications;
+        p->pBmc->pAigFrames->pImpData = p->pBmc;
+        p->pBmc->vImps = p->pCla->vImps;
+        nImpsOld = Vec_IntSize(p->pCla->vImps);
+    } 
+    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
+    p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
+    p->pBmc->pAigFrames->pObjCopies = NULL;
     // annotate frames nodes with pointers to the manager
     Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
         pObj->pData = p;
@@ -271,19 +315,31 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
             Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
             Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
         PRT( "Time", clock() - clk );
-        printf( "Before BMC: " );  Fra_ClassesPrint( p->pCla, 0 );
+        printf( "Before BMC: " );  
+//        Fra_ClassesPrint( p->pCla, 0 );
+        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
+            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
+        if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+            printf( "Imp = %5d. ", nImpsOld );
+        printf( "\n" );
     }
     // refine the classes
     p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
     p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
     Fra_ClassesRefine( p->pCla );
-    Fra_ClassesRefine1( p->pCla );
+    Fra_ClassesRefine1( p->pCla, 1, NULL );
     p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
     p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
     // report the results
     if ( p->pPars->fVerbose )
     {
-        printf( "After  BMC: " );  Fra_ClassesPrint( p->pCla, 0 );
+        printf( "After  BMC: " );  
+//        Fra_ClassesPrint( p->pCla, 0 );
+        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
+            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
+        if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+            printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
+        printf( "\n" );
     }
     // free the BMC manager
     Fra_BmcStop( p->pBmc );  
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index d6db125b..3e3392c7 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -520,10 +520,10 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_ClassesRefine1( Fra_Cla_t * p )
+int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
 {
     Aig_Obj_t * pObj, ** ppClass;
-    int i, k, nRefis;
+    int i, k, nRefis = 1;
     // check if there is anything to refine
     if ( Vec_PtrSize(p->vClasses1) == 0 )
         return 0;
@@ -565,7 +565,10 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     assert( ppClass[0] != NULL );
     Vec_PtrPush( p->vClasses, ppClass );
     // iteratively refine this class
-    nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
+    if ( fRefineNewClass )
+        nRefis += Fra_RefineClassLastIter( p, p->vClasses );
+    else if ( pSkipped )
+        (*pSkipped)++;
     return nRefis;
 }
 
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 9adbb7a9..94beb61a 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -246,7 +246,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Vec_PtrPush( p->vTimeouts, pObj );
     // verify that the counter-example satisfies all the constraints
 //    if ( p->vCex )
-//    Fra_FraigVerifyCounterEx( p, p->vCex );
+//        Fra_FraigVerifyCounterEx( p, p->vCex );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
     if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
@@ -334,12 +334,15 @@ clk = clock();
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
     // collect initial states
-    p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
     // perform fraig sweep
     Fra_FraigSweep( p );
+    // call back the procedure to check implications
+    if ( pManAig->pImpFunc )
+        pManAig->pImpFunc( p, pManAig->pImpData );
+    // finalize the fraiged manager
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
     {
@@ -397,6 +400,32 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
     pPars->fChoicing    = 1;
     return Fra_FraigPerform( pManAig, pPars );
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
+{
+    Aig_Man_t * pFraig;
+    Fra_Par_t Pars, * pPars = &Pars; 
+    Fra_ParamsDefault( pPars );
+    pPars->nBTLimitNode = nConfMax;
+    pPars->fVerbose     = 0;
+    pPars->fProve       = 0;
+    pPars->fDoSparse    = 1;
+    pPars->fSpeculate   = 0;
+    pPars->fChoicing    = 0;
+    pFraig = Fra_FraigPerform( pManAig, pPars );
+    return pFraig;
+} 
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 8af11b78..5e4b8c28 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -24,10 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int   Sml_ImpLeft( int Imp )               { return Imp & 0xFFFF;         }
-static inline int   Sml_ImpRight( int Imp )              { return Imp >> 16;            }
-static inline int   Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -43,19 +39,35 @@ static inline int   Sml_ImpCreate( int Left, int Right ) { return (Right << 16)
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
+{
+    unsigned * pSim;
+    int k, Counter = 0;
+    pSim = Fra_ObjSim( p, Node );
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSim[k] );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1s in each siminfo of each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj;
-    unsigned * pSim;
-    int i, k, * pnBits; 
+    int i, * pnBits; 
     pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );  
     memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
     Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        pSim = Fra_ObjSim( p, i );
-        for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-            pnBits[i] += Aig_WordCountOnes( pSim[k] );
-    }
+        pnBits[i] = Fra_SmlCountOnesOne( p, i );
     return pnBits;
 }
 
@@ -106,6 +118,27 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of 1s in the reverse implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
+{
+    unsigned * pSimL, * pSimR;
+    int k;
+    pSimL = Fra_ObjSim( p, Left );
+    pSimR = Fra_ObjSim( p, Right );
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        pResult[k] |= pSimL[k] & ~pSimR[k];
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the array of nodes sorted by the number of 1s.]
 
   Description []
@@ -284,7 +317,6 @@ int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
 ***********************************************************************/
 Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
 {
-//    Aig_Obj_t * pObj;
     int nSimWords = 64;
     Fra_Sml_t * pSeq, * pComb;
     Vec_Int_t * vImps, * vTemp;
@@ -293,21 +325,13 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = AIG_INFINITY, CostMax = 0;
     int i, k, Imp, CostRange, clk = clock();
+    assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) );
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
     pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
     // get the nodes sorted by the number of 1s
     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
-/*
-Aig_ManForEachObj( p->pManAig, pObj, i )
-{
-    printf( "%6s", Aig_ObjIsPi(pObj)? "pi" : (Aig_ObjIsNode(pObj)? "node" : "other" ) );
-    printf( "%d (%d) :\n", i, pObj->fPhase );
-    Extra_PrintBinary( stdout, Fra_ObjSim( pComb, i ), 64 ); printf( "\n" );
-    Extra_PrintBinary( stdout, Fra_ObjSim( pSeq, i ), 64 ); printf( "\n" );
-}
-*/
     // count the total number of implications
     for ( k = nSimWords * 32; k > 0; k-- )
     for ( i = k - 1; i > 0; i-- )
@@ -335,10 +359,8 @@ Aig_ManForEachObj( p->pManAig, pObj, i )
                     nImpsComb++;
                     continue;
                 }
-//                printf( "d=%d c=%d  ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) );
- 
                 nImpsCollected++;
-                Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
+                Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
                 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
                 CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
                 CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
@@ -368,13 +390,16 @@ finish:
             (int (*)(const void *, const void *)) Sml_CompareMaxId );
 if ( p->pPars->fVerbose )
 {
-printf( "Tot = %d. Try = %d. NonS = %d. C = %d. Found = %d.  Cost = [%d < %d < %d] ", 
-    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostRange, CostMax );
+printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
+    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
+printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
+       CostMin, CostRange, CostMax );
 PRT( "Time", clock() - clk );
 }
     return vImps;
 }
 
+
 // the following three procedures are called to 
 // - add implications to the SAT solver
 // - check implications using the SAT solver
@@ -401,8 +426,8 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
     Vec_IntForEachEntry( vImps, Imp, i )
     {
         // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
         // check if all the nodes are present
         for ( f = 0; f < p->pPars->nFramesK; f++ )
         {
@@ -431,7 +456,7 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
             // get the complemented attributes
             fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
             fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
-            // get the constaint
+            // get the constraint
             // L => R      L' v R     (complement = L & R')
             pLits[0] = 2 * Left  + !fComplL;
             pLits[1] = 2 * Right +  fComplR;
@@ -476,8 +501,8 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
     {
         if ( Imp == 0 )
             continue;
-        Left = Sml_ImpLeft(Imp);
-        Right = Sml_ImpRight(Imp);
+        Left = Fra_ImpLeft(Imp);
+        Right = Fra_ImpRight(Imp);
         Max = AIG_MAX( Left, Right );
         assert( Max >= pNode->Id );
         if ( Max > pNode->Id )
@@ -494,9 +519,6 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
         // check equality
         if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
         {
-//            assert( fComplL == fComplR );
-//            if ( fComplL != fComplR )
-//                printf( "Fra_ImpCheckForNode(): Unexpected situation!\n" );
             if ( fComplL != fComplR )
                 Vec_IntWriteEntry( vImps, i, 0 );
             continue;
@@ -507,6 +529,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
         // make sure the implication is refined
         if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
         {
+            p->pCla->fRefinement = 1;
             Fra_SmlResimulate( p );
             if ( Vec_IntEntry(vImps, i) != 0 )
                 printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
@@ -536,8 +559,8 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
         if ( Imp == 0 )
             continue;
         // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
         // check if implication holds using this simulation info
         if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
         {
@@ -569,6 +592,113 @@ void Fra_ImpCompactArray( Vec_Int_t * vImps )
     Vec_IntShrink( vImps, k );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Determines the ratio of the state space by computed implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
+{
+    int nSimWords = 64;
+    Fra_Sml_t * pComb;
+    unsigned * pResult;
+    double Ratio = 0.0;
+    int Left, Right, Imp, i;
+    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+        return Ratio;
+    // simulate the AIG manager with combinational patterns
+    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
+    // go through the implications and collect where they do not hold
+    pResult = Fra_ObjSim( pComb, 0 );
+    assert( pResult[0] == 0 );
+    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+    {
+        Left = Fra_ImpLeft(Imp);
+        Right = Fra_ImpRight(Imp);
+        Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
+    }
+    // count the number of ones in this area
+    Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
+    Fra_SmlStop( pComb );
+    return Ratio;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of failed implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
+{
+    int nSimWords = 2000;
+    Fra_Sml_t * pSeq;
+    char * pfFails;
+    int Left, Right, Imp, i, Counter;
+    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+        return 0;
+    // simulate the AIG manager with combinational patterns
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 );
+    // go through the implications and check how many of them do not hold
+    pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
+    memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
+    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+    {
+        Left = Fra_ImpLeft(Imp);
+        Right = Fra_ImpRight(Imp);
+        pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
+    }
+    // count how many has failed
+    Counter = 0;
+    for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
+        Counter += pfFails[i];
+    free( pfFails );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Record proven implications in the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pLeft, * pRight, * pMiter;
+    int nPosOld, Imp, i;
+    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
+        return;
+    // go through the implication
+    nPosOld = Aig_ManPoNum(pNew);
+    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
+    {
+        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
+        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
+        // record the implication: L' + R
+        pMiter = Aig_Or( pNew, 
+            Aig_NotCond(pLeft->pData, !pLeft->fPhase), 
+            Aig_NotCond(pRight->pData, pRight->fPhase) ); 
+        Aig_ObjCreatePo( pNew, pMiter );
+    }
+    pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 6d8305c0..53dbdbb6 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -177,6 +177,61 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
+{
+    Aig_Obj_t * pObj, ** pLatches;
+    int i, k, f, nNodesOld;
+    // set copy pointer of each object to point to itself
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->pData = pObj;
+    // iterate and add objects
+    nNodesOld = Aig_ManObjIdMax(p);
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // clean latch inputs and outputs
+        Aig_ManForEachLiSeq( p, pObj, i )
+            pObj->pData = NULL;
+        Aig_ManForEachLoSeq( p, pObj, i )
+            pObj->pData = NULL;
+        // save the latch input values
+        k = 0;
+        Aig_ManForEachLiSeq( p, pObj, i )
+        {
+            if ( Aig_ObjFanin0(pObj)->pData )
+                pLatches[k++] = Aig_ObjChild0Copy(pObj);
+            else
+                pLatches[k++] = NULL;
+        }
+        // insert them as the latch output values
+        k = 0;
+        Aig_ManForEachLoSeq( p, pObj, i )
+            pObj->pData = pLatches[k++];
+        // create the next time frame of nodes
+        Aig_ManForEachNode( p, pObj, i )
+        {
+            if ( i > nNodesOld )
+                break;
+            if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
+                pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            else
+                pObj->pData = NULL;
+        }
+    }
+    free( pLatches );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs choicing of the AIG.]
 
   Description []
@@ -186,7 +241,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -201,8 +256,9 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pManAigNew;
-//    Vec_Int_t * vImps;
+    int nNodesBeg, nRegsBeg, Temp;
     int nIter, i, clk = clock(), clk2;
+
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
@@ -212,6 +268,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( nFramesK > 0 );
 //Aig_ManShow( pManAig, 0, NULL );
+ 
+    nNodesBeg = Aig_ManNodeNum(pManAig);
+    nRegsBeg  = Aig_ManRegNum(pManAig);
+
+    // enhance the AIG by adding timeframes
+//    Fra_FramesAddMore( pManAig, 3 );
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
@@ -222,6 +284,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
     pPars->fUseImps   = fUseImps;
+    pPars->fWriteImps = fWriteImps;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
@@ -255,19 +318,19 @@ PRT( "Time", clock() - clk );
         p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
     }
 
-    // perform BMC (for the min number of frames)
-    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK );
-//Fra_ClassesPrint( p->pCla, 1 );
-//    p->vCex = Vec_IntAlloc( 1000 );
-
     // select the most expressive implications
     if ( pPars->fUseImps )
         p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
- 
-    p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
+
+    // perform BMC (for the min number of frames)
+    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
+//Fra_ClassesPrint( p->pCla, 1 );
+//    if ( p->vCex == NULL )
+//        p->vCex = Vec_IntAlloc( 1000 );
+
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesBeg = Aig_ManNodeNum(pManAig);
-    p->nRegsBeg  = Aig_ManRegNum(pManAig);
+    p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
+    p->nRegsBeg  = nRegsBeg; // Aig_ManRegNum(pManAig);
 
     // dump AIG of the timeframes
 //    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
@@ -279,6 +342,8 @@ PRT( "Time", clock() - clk );
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
     {
+        int nLitsOld = Fra_ClassesCountLits(p->pCla);
+        int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
         // mark the classes as non-refined
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
@@ -325,13 +390,13 @@ PRT( "Time", clock() - clk );
         // report the intermediate results
         if ( fVerbose )
         {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  %s = %6d. NR = %6d.\n", 
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
-                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
-                p->pCla->vImps? "I" : "N", 
-                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig), 
-                Aig_ManNodeNum(p->pManFraig) );
-        }
+                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
+            if ( p->pCla->vImps )
+                printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
+            printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) );
+        } 
 
         // perform sweeping
         p->nSatCallsRecent = 0;
@@ -341,18 +406,40 @@ PRT( "Time", clock() - clk );
         assert( p->vTimeouts == NULL );
         if ( p->vTimeouts )
            printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
-
         // cleanup
         Fra_ManClean( p );
-//        if ( nIter == 3 )
-//            break;
+        // check if refinement has happened
+//        p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
+        if ( p->pCla->fRefinement && 
+            nLitsOld == Fra_ClassesCountLits(p->pCla) && 
+            nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) )
+        {
+            printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
+            break;
+        }
     }
-//    Fra_ClassesPrint( p->pCla, 1 );
-//    Fra_ClassesSelectRepr( p->pCla );
+    // check implications using simulation
+    if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
+    {
+        int clk = clock();
+        if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
+            printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
+        else
+            printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
+        PRT( "Time", clock() - clk );
+    }
+
+
     // move the classes into representatives and reduce AIG
 clk2 = clock();
+//    Fra_ClassesPrint( p->pCla, 1 );
+    Fra_ClassesSelectRepr( p->pCla );
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
     pManAigNew = Aig_ManDupRepr( pManAig );
+    // add implications to the manager
+    if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
+        Fra_ImpRecordInManager( p, pManAigNew );
+    // cleanup the new manager
     Aig_ManSeqCleanup( pManAigNew );
 //    Aig_ManCountMergeRegs( pManAigNew );
 p->timeTrav += clock() - clk2;
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
new file mode 100644
index 00000000..c3b5504e
--- /dev/null
+++ b/src/aig/fra/fraLcr.c
@@ -0,0 +1,644 @@
+/**CFile****************************************************************
+
+  FileName    [fraLcorr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Latch correspondence computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Fra_Lcr_t_    Fra_Lcr_t;
+struct Fra_Lcr_t_
+{
+    // original AIG
+    Aig_Man_t *      pAig;
+    // equivalence class representation
+    Fra_Cla_t *      pCla;       
+    // partitioning information
+    Vec_Ptr_t *      vParts;        // output partitions
+    int *            pInToOutPart;  // mapping of PI num into PO partition num
+    int *            pInToOutNum;   // mapping of PI num into the num of this PO in the partition
+    // AIGs for the partitions
+    Vec_Ptr_t *      vFraigs;
+    // other variables
+    int              fRefining; 
+    // parameters
+    int              nFramesP;
+    int              fVerbose;
+    // statistics
+    int              nIters;
+    int              nLitsBeg;
+    int              nLitsEnd;
+    int              nNodesBeg;
+    int              nNodesEnd;
+    int              nRegsBeg;
+    int              nRegsEnd;
+    // runtime
+    int              timeSim;
+    int              timePart;
+    int              timeTrav;
+    int              timeFraig;
+    int              timeUpdate;
+    int              timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the retiming manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
+{
+    Fra_Lcr_t * p;
+    p = ALLOC( Fra_Lcr_t, 1 );
+    memset( p, 0, sizeof(Fra_Lcr_t) );
+    p->pAig = pAig;
+    p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
+    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+    p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
+    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+    p->vFraigs = Vec_PtrAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lcr_ManPrint( Fra_Lcr_t * p )
+{
+    printf( "Iterations = %d.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
+        p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
+    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
+        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
+        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
+    PRT( "AIG simulation  ", p->timeSim  );
+    PRT( "AIG partitioning", p->timePart );
+    PRT( "AIG rebuiding   ", p->timeTrav );
+    PRT( "FRAIGing        ", p->timeFraig );
+    PRT( "AIG updating    ", p->timeUpdate );
+    PRT( "TOTAL RUNTIME   ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the retiming manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lcr_ManFree( Fra_Lcr_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    if ( p->fVerbose )
+        Lcr_ManPrint( p );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        pObj->pNext = NULL;
+    Vec_PtrFree( p->vFraigs );
+    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
+    if ( p->vParts  )   Vec_VecFree( (Vec_Vec_t *)p->vParts );
+    free( p->pInToOutPart );
+    free( p->pInToOutNum );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepare the AIG for class computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
+{
+    Fra_Man_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    p = ALLOC( Fra_Man_t, 1 );
+    memset( p, 0, sizeof(Fra_Man_t) );
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = p;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepare the AIG for class computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares two nodes for equivalence after partitioned fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    Fra_Man_t * pTemp = pObj0->pData;
+    Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
+    Aig_Man_t * pFraig;
+    Aig_Obj_t * pOut0, * pOut1;
+    int nPart0, nPart1;
+    assert( Aig_ObjIsPi(pObj0) );
+    assert( Aig_ObjIsPi(pObj1) );
+    // find the partition to which these nodes belong
+    nPart0 = pLcr->pInToOutPart[(int)pObj0->pNext];
+    nPart1 = pLcr->pInToOutPart[(int)pObj1->pNext];
+    // if this is the result of refinement of the class created const-1 nodes
+    // the nodes may end up in different partions - we assume them equivalent
+    if ( nPart0 != nPart1 )
+    {
+        assert( 0 );
+        return 1;
+    }
+    assert( nPart0 == nPart1 );
+    pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 );
+    // get the fraig outputs
+    pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj0->pNext] );
+    pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj1->pNext] );
+    return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the node with a constant after partioned fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
+{
+    Fra_Man_t * pTemp = pObj->pData;
+    Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
+    Aig_Man_t * pFraig;
+    Aig_Obj_t * pOut;
+    int nPart;
+    assert( Aig_ObjIsPi(pObj) );
+    // find the partition to which these nodes belong
+    nPart = pLcr->pInToOutPart[(int)pObj->pNext];
+    pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart );
+    // get the fraig outputs
+    pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj->pNext] );
+    return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Give the AIG and classes, reduces AIG for partitioning.]
+
+  Description [Ignores registers that are not in the classes. 
+  Places candidate equivalent classes of registers into single outputs 
+  (for ease of partitioning). The resulting combinational AIG contains 
+  outputs in the same order as equivalence classes of registers, 
+  followed by constant-1 registers. Preserves the set of all inputs.
+  Complemented attributes of the outputs do not matter because we need 
+  then only for collecting the structural info.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
+    int i, c, Offset;
+    // remember the numbers of the inputs of the original AIG
+    Aig_ManForEachPi( pLcr->pAig, pObj, i )
+    {
+        pObj->pData = pLcr;
+        pObj->pNext = (Aig_Obj_t *)i;
+    }
+    // compute the LO/LI offset
+    Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
+    // create the PIs
+    Aig_ManCleanData( pLcr->pAig );
+    pNew = Aig_ManStartFrom( pLcr->pAig );
+    // go over the equivalence classes
+    Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i )
+    {
+        pMiter = Aig_ManConst0(pNew);
+        for ( c = 0; ppClass[c]; c++ )
+        {
+            assert( Aig_ObjIsPi(ppClass[c]) );
+            pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(int)ppClass[c]->pNext );
+            pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+            pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
+        }
+        Aig_ObjCreatePo( pNew, pMiter );
+    }
+    // go over the constant candidates
+    Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i )
+    {
+        assert( Aig_ObjIsPi(pObj) );
+        pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)pObj->pNext );
+        pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+        Aig_ObjCreatePo( pNew, pMiter );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps partitions into the inputs of original AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOutPart, int * pInToOutNum )
+{
+    Vec_Int_t * vOne, * vOneNew;
+    Aig_Obj_t ** ppClass, * pObjPi;
+    int Out, Offset, i, k, c;
+    // compute the LO/LI offset
+    Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
+    Vec_PtrForEachEntry( vParts, vOne, i )
+    {
+        vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
+        Vec_IntForEachEntry( vOne, Out, k )
+        {
+            if ( Out < Vec_PtrSize(pCla->vClasses) )
+            {
+                ppClass = Vec_PtrEntry( pCla->vClasses, Out );
+                for ( c = 0; ppClass[c]; c++ )
+                {
+                    pInToOutPart[(int)ppClass[c]->pNext] = i;
+                    pInToOutNum[(int)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
+                    Vec_IntPush( vOneNew, Offset+(int)ppClass[c]->pNext );
+                }
+            }
+            else
+            {
+                pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
+                pInToOutPart[(int)pObjPi->pNext] = i;
+                pInToOutNum[(int)pObjPi->pNext] = Vec_IntSize(vOneNew);
+                Vec_IntPush( vOneNew, Offset+(int)pObjPi->pNext );
+            }
+        }
+        // replace the class
+        Vec_PtrWriteEntry( vParts, i, vOneNew );
+        Vec_IntFree( vOne );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG of one partition with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->pData;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+//        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
+        Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
+        if ( pRepr == NULL )
+            pObj->pData = Aig_ObjCreatePi( pNew );
+        else
+        {
+            pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
+            pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase );
+        }
+        return pObj->pData;
+    }
+    Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
+    Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
+    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG of one partition with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int Out, i;
+    // create new AIG for this partition
+    pNew = Aig_ManStartFrom( p->pAig );
+    Aig_ManIncrementTravId( p->pAig );
+    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
+    Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
+    Vec_IntForEachEntry( vPart, Out, i )
+    {
+        pObj = Aig_ManPo( p->pAig, Out );
+        if ( pObj->fMarkA )
+        {
+            pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
+            pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
+        }
+        else
+            pObjNew = Aig_ManConst1( pNew );
+        Aig_ObjCreatePo( pNew, pObjNew ); 
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes belonging to the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassNodesMark( Fra_Lcr_t * p )
+{
+    Aig_Obj_t * pObj, ** ppClass;
+    int i, c, Offset;
+    // compute the LO/LI offset
+    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+    // mark the nodes remaining in the classes
+    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    {
+        pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
+        pObj->fMarkA = 1;
+    }
+    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    {
+        for ( c = 0; ppClass[c]; c++ )
+        {
+            pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
+            pObj->fMarkA = 1;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the nodes belonging to the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
+{
+    Aig_Obj_t * pObj, ** ppClass;
+    int i, c, Offset;
+    // compute the LO/LI offset
+    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+    // mark the nodes remaining in the classes
+    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
+    {
+        pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
+        pObj->fMarkA = 0;
+    }
+    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
+    {
+        for ( c = 0; ppClass[c]; c++ )
+        {
+            pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
+            pObj->fMarkA = 0;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs choicing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter )
+{
+    int nPartSize    = 200;
+    int fReprSelect  = 0;
+
+    Fra_Lcr_t * p;
+    Fra_Man_t * pTemp;
+    Aig_Man_t * pAigPart, * pAigNew = NULL;
+    Vec_Int_t * vPart;
+    Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
+    int i, nIter, clk = clock(), clk2, clk3;
+    if ( Aig_ManNodeNum(pAig) == 0 )
+    {
+        if ( pnIter ) *pnIter = 0;
+        return Aig_ManDup(pAig, 1);
+    }
+    assert( Aig_ManLatchNum(pAig) == 0 );
+    assert( Aig_ManRegNum(pAig) > 0 );
+
+    // start the manager
+    p = Lcr_ManAlloc( pAig );
+    p->nFramesP = nFramesP;
+    p->fVerbose = fVerbose;
+
+    // simulate the AIG 
+clk2 = clock();
+if ( fVerbose )
+printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
+    pTemp = Fra_LcrAigPrepare( p->pAig );
+    pTemp->pBmc = (Fra_Bmc_t *)p;
+    pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 ); 
+if ( fVerbose ) 
+{
+PRT( "Time", clock() - clk2 );
+p->timeSim += clock() - clk2;
+}
+    // get preliminary info about equivalence classes
+    pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
+    Fra_ClassesPrepare( p->pCla, 1 );
+    p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
+    p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
+    Fra_SmlStop( pTemp->pSml );
+
+    // partition the AIG for latch correspondence computation
+clk2 = clock();
+if ( fVerbose )
+printf( "Partitioning AIG ...  " );
+    pAigPart = Fra_LcrDeriveAigForPartitioning( p );
+    p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
+    Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
+    Aig_ManStop( pAigPart );
+if ( fVerbose ) 
+{
+PRT( "Time", clock() - clk2 );
+p->timePart += clock() - clk2;
+}
+
+    // get the initial stats
+    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
+    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
+    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
+
+    // perforn interative reduction of the partitions
+    p->fRefining = 1;
+    for ( nIter = 0; p->fRefining; nIter++ )
+    {
+        p->fRefining = 0;
+        clk3 = clock();
+        // derive AIGs for each partition
+        Fra_ClassNodesMark( p );
+        Vec_PtrClear( p->vFraigs );
+        Vec_PtrForEachEntry( p->vParts, vPart, i )
+        {
+clk2 = clock();
+            pAigPart = Fra_LcrCreatePart( p, vPart );
+p->timeTrav += clock() - clk2;
+clk2 = clock();
+            pAigNew  = Fra_FraigEquivence( pAigPart, nConfMax );
+p->timeFraig += clock() - clk2;
+            Vec_PtrPush( p->vFraigs, pAigNew );
+            Aig_ManStop( pAigPart );
+        }
+        Fra_ClassNodesUnmark( p );
+        // report the intermediate results
+        if ( fVerbose )
+        {
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
+                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
+                Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
+            PRT( "T", clock() - clk3 );
+        }
+        // refine the classes
+        Fra_LcrAigPrepareTwo( p->pAig, pTemp );
+        if ( Fra_ClassesRefine( p->pCla ) )
+            p->fRefining = 1;
+        if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
+            p->fRefining = 1;
+        // clean the fraigs
+        Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
+            Aig_ManStop( pAigPart );
+
+        // repartition if needed
+        if ( 1 )
+        {
+clk2 = clock();
+            Vec_VecFree( (Vec_Vec_t *)p->vParts );
+            pAigPart = Fra_LcrDeriveAigForPartitioning( p );
+            p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
+            Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
+            Aig_ManStop( pAigPart );
+p->timePart += clock() - clk2;
+        }
+    }
+    free( pTemp );
+    p->nIters = nIter;
+
+    // move the classes into representatives and reduce AIG
+clk2 = clock();
+//    Fra_ClassesPrint( p->pCla, 1 );
+    if ( fReprSelect )
+        Fra_ClassesSelectRepr( p->pCla );
+    Fra_ClassesCopyReprs( p->pCla, NULL );
+    pAigNew = Aig_ManDupRepr( p->pAig );
+    Aig_ManSeqCleanup( pAigNew );
+//    Aig_ManCountMergeRegs( pAigNew );
+p->timeUpdate += clock() - clk2;
+p->timeTotal = clock() - clk;
+    // get the final stats
+    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
+    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
+    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
+    Lcr_ManFree( p );
+    if ( pnIter ) *pnIter = nIter;
+    return pAigNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 0116bbc4..97282e98 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -181,6 +181,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
     assert( p->pManFraig == NULL );
     // start the fraig package
     pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
+    pManFraig->nRegs    = p->pManAig->nRegs;
+    pManFraig->nAsserts = p->pManAig->nAsserts;
     // set the pointers to the available fraig nodes
     Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
     Aig_ManForEachPi( p->pManAig, pObj, i )
@@ -271,9 +273,9 @@ void Fra_ManPrint( Fra_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
     printf( "SimWord = %d. Round = %d.  Mem = %0.2f Mb.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
-        p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
-    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars );
+        p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
+    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 8b9258cb..88c552dc 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pNew;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
@@ -48,7 +48,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -56,7 +56,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
@@ -89,6 +89,136 @@ PRT( "Time", clock() - clkTotal );
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+{
+    Aig_Man_t * pNew, * pTemp;
+    int nFrames, RetValue, nIter, clk, clkTotal = clock();
+    int fLatchCorr = 0;
+
+    pNew = Aig_ManDup( p, 1 );
+    if ( fVerbose )
+    {
+        printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
+            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+    }
+//Aig_ManDumpBlif( pNew, "after.blif" );
+
+    // perform sequential cleanup
+clk = clock();
+    pNew = Aig_ManReduceLaches( pNew, 0 );
+    pNew = Aig_ManConstReduce( pNew, 0 );
+    if ( fVerbose )
+    {
+        printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
+            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+    }
+
+    // perform forward retiming
+    if ( fRetimeFirst )
+    {
+clk = clock();
+    pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose )
+    {
+        printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
+            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+    }
+    }
+    
+    // run latch correspondence
+clk = clock();
+    pNew = Aig_ManDup( pTemp = pNew, 1 );
+    Aig_ManStop( pTemp );
+    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
+    Aig_ManStop( pTemp );
+    if ( fVerbose )
+    {
+        printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
+            nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+    }
+
+    // perform fraiging
+clk = clock();
+    pNew = Fra_FraigEquivence( pTemp = pNew, 1000 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose )
+    {
+        printf( "Fraiging:             Latches = %5d. Nodes = %6d. ", 
+            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+    }
+
+    // perform seq sweeping while increasing the number of frames
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue == -1 )
+    for ( nFrames = 1; ; nFrames *= 2 )
+    {
+clk = clock();
+        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
+        Aig_ManStop( pTemp );
+        RetValue = Fra_FraigMiterStatus( pNew );
+        if ( fVerbose )
+        { 
+            printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
+                nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        }
+        if ( RetValue != -1 )
+            break;
+        // perform rewriting
+clk = clock();
+        pNew = Aig_ManDup( pTemp = pNew, 1 );
+        Aig_ManStop( pTemp );
+        pNew = Dar_ManRewriteDefault( pTemp = pNew );
+        if ( fVerbose )
+        {
+            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        }
+        // perform retiming
+clk = clock();
+        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+        Aig_ManStop( pTemp );
+        pNew = Aig_ManDup( pTemp = pNew, 1 );
+        Aig_ManStop( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        }
+    }
+    // get the miter status
+    RetValue = Fra_FraigMiterStatus( pNew );
+    Aig_ManStop( pNew );
+
+    // report the miter
+    if ( RetValue == 1 )
+        printf( "Networks are equivalent.   " );
+    else if ( RetValue == 0 )
+        printf( "Networks are NOT EQUIVALENT.   " );
+    else
+        printf( "Networks are UNDECIDED.   " );
+PRT( "Time", clock() - clkTotal );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 3463ee0d..0b93fb73 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -199,7 +199,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
     Aig_ManForEachPi( p->pManFraig, pObj, i )
         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
             Aig_InfoSetBit( p->pPatWords, i );
-/*
+
     if ( p->vCex )
     {
         Vec_IntClear( p->vCex );
@@ -208,7 +208,6 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
         for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
             Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
     }
-*/
 
 /*
     printf( "Pattern: " );
@@ -608,7 +607,7 @@ void Fra_SmlResimulate( Fra_Man_t * p )
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
-    nChanges += Fra_ClassesRefine1( p->pCla );
+    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
     if ( p->pCla->vImps )
         nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
 p->timeRef += clock() - clk;
@@ -652,7 +651,7 @@ printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
-    nChanges += Fra_ClassesRefine1( p->pCla );
+    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
 p->timeRef += clock() - clk;
 if ( fVerbose )
 printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
@@ -663,7 +662,7 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
-    nChanges += Fra_ClassesRefine1( p->pCla );
+    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
 p->timeRef += clock() - clk;
 
 if ( fVerbose )
@@ -677,7 +676,7 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
             return;
 clk = clock();
         nChanges = Fra_ClassesRefine( p->pCla );
-        nChanges += Fra_ClassesRefine1( p->pCla );
+        nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
 p->timeRef += clock() - clk;
 if ( fVerbose )
 printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
@@ -704,7 +703,6 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
 Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
 {
     Fra_Sml_t * p;
-    assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
     p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
     memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
     p->pAig        = pAig;
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index bd8a20be..e7264fdc 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -5,6 +5,7 @@ SRC +=    src/aig/fra/fraBmc.c \
     src/aig/fra/fraCore.c \
     src/aig/fra/fraImp.c \
     src/aig/fra/fraInd.c \
+    src/aig/fra/fraLcr.c \
     src/aig/fra/fraMan.c \
     src/aig/fra/fraSat.c \
     src/aig/fra/fraSec.c \