Version abc70828

33 files changed, 2220 insertions, 560 deletions

diff --git a/abc.dsp b/abc.dsp
index 17c2006a..c4f6e05f 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2586,6 +2586,10 @@ SOURCE=.\src\aig\fra\fraInd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\fra\fraLcr.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\fra\fraMan.c
 # End Source File
 # Begin Source File
@@ -2794,6 +2798,10 @@ SOURCE=.\src\aig\aig\aigRet.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigScl.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigSeq.c
 # End Source File
 # Begin Source File
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 \
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index bda8781c..42820550 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -869,6 +869,7 @@ extern void *             Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFree
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index bb1ae2ed..b4a97223 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -148,6 +148,33 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads the number of cubes of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, nCubes, nCubePairs = 0;
+    assert( Abc_NtkHasSop(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        assert( pNode->pData );
+        nCubes = Abc_SopGetCubeNum( pNode->pData );
+        nCubePairs += nCubes * (nCubes - 1) / 2;
+    }
+    return nCubePairs;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of literals in the SOPs of the nodes.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 78519d40..3902830d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -123,6 +123,7 @@ static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCSweep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -166,6 +167,7 @@ static int Abc_CommandRetime         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLcorr          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -326,12 +328,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "zero",          Abc_CommandZero,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
-//    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
-//    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "lcorr",         Abc_CommandLcorr,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
@@ -339,6 +340,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsec",          Abc_CommandDSec,             0 );
+    Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
@@ -2588,22 +2590,34 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     p = ALLOC( Fxu_Data_t, 1 );
     memset( p, 0, sizeof(Fxu_Data_t) );
     // set the defaults
-    p->nPairsMax = 30000;
-    p->nNodesExt = 10000;
-    p->fOnlyS    = 0;
-    p->fOnlyD    = 0;
-    p->fUse0     = 0;
-    p->fUseCompl = 1;
-    p->fVerbose  = 0;
+    p->nSingleMax = 20000;
+    p->nPairsMax  = 30000;
+    p->nNodesExt  = 10000;
+    p->fOnlyS     = 0;
+    p->fOnlyD     = 0;
+    p->fUse0      = 0;
+    p->fUseCompl  = 1;
+    p->fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "LNsdzcvh")) != EOF ) 
+    while ( (c = Extra_UtilGetopt(argc, argv, "SDNsdzcvh")) != EOF ) 
     {
         switch (c) 
         {
-            case 'L':
+            case 'S':
                 if ( globalUtilOptind >= argc )
                 {
-                    fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                    fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                p->nSingleMax = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( p->nSingleMax < 0 ) 
+                    goto usage;
+                break;
+            case 'D':
+                if ( globalUtilOptind >= argc )
+                {
+                    fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
                     goto usage;
                 }
                 p->nPairsMax = atoi(argv[globalUtilOptind]);
@@ -2643,7 +2657,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
             default:
                 goto usage;
         }
-    }
+    } 
 
     if ( pNtk == NULL )
     {
@@ -2673,10 +2687,11 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fx [-N num] [-L num] [-sdzcvh]\n");
+    fprintf( pErr, "usage: fx [-S num] [-D num] [-N num] [-sdzcvh]\n");
     fprintf( pErr, "\t         performs unate fast extract on the current network\n");
+    fprintf( pErr, "\t-S num : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );  
+    fprintf( pErr, "\t-D num : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );  
     fprintf( pErr, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );  
-    fprintf( pErr, "\t-L num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax );  
     fprintf( pErr, "\t-s     : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );  
     fprintf( pErr, "\t-d     : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );  
     fprintf( pErr, "\t-z     : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );  
@@ -6175,7 +6190,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLevels = 128;
+    nLevels = 1000;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
     {
@@ -6293,7 +6308,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
 //    pNtkRes = Abc_NtkDar( pNtk );
-    pNtkRes = Abc_NtkDarRetime( pNtk, 1000, 1 );
+    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8674,7 +8689,7 @@ int Abc_CommandFraigDress( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose = 1;
+    fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
@@ -10975,12 +10990,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFramesP;
     int nFramesK;
     int nMaxImps;
-    int fExdc;
     int fUseImps;
     int fRewrite;
     int fLatchCorr;
+    int fWriteImps;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10990,13 +11005,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFramesP   = 0;
     nFramesK   = 1;
     nMaxImps   = 5000;
-    fExdc      = 1;
     fUseImps   = 0;
     fRewrite   = 0;
     fLatchCorr = 0;
+    fWriteImps = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PFIeirlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PFIirlevh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -11033,9 +11048,6 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nMaxImps <= 0 ) 
                 goto usage;
             break;
-        case 'e':
-            fExdc ^= 1;
-            break;
         case 'i':
             fUseImps ^= 1;
             break;
@@ -11045,6 +11057,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fLatchCorr ^= 1;
             break;
+        case 'e':
+            fWriteImps ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -11069,12 +11084,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Sequential sweep works only for structurally hashed networks (run \"strash\").\n" );
-        return 1;
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11085,15 +11100,120 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
     fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
-//    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
+    fprintf( pErr, "\t-e     : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nFramesP;
+    int nConfMax;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFramesP   = 0;
+    nConfMax   = 10000;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesP < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkDarLcorr( pNtk, nFramesP, nConfMax, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential sweeping has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: lcorr [-P num] [-C num] [-vh]\n" );
+    fprintf( pErr, "\t         computes latch correspondence using 1-step induction\n" );
+    fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
+    fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -11113,12 +11233,12 @@ usage:
 int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes, * pTemp;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int fLatchSweep;
     int fAutoSweep;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11153,23 +11273,13 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsLogic(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Only works for logic networks.\n" );
+        fprintf( pErr, "Only works for structrally hashed networks.\n" );
         return 1;
     }
     // modify the current network
-
-    // get the new network
-    pNtkRes = Abc_NtkDup( pNtk ); 
-    Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose );
-    if ( fLatchSweep )
-    {
-        pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 );
-        Abc_NtkDelete( pTemp );
-        pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose );
-        Abc_NtkDelete( pTemp );
-    }
+    pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential cleanup has failed.\n" );
@@ -11180,14 +11290,14 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scleanup [-lavh]\n" );
+    fprintf( pErr, "usage: scleanup [-lvh]\n" );
     fprintf( pErr, "\t         performs sequential cleanup\n" );
     fprintf( pErr, "\t         - removes nodes/latches that do not feed into POs\n" );
     fprintf( pErr, "\t         - removes stuck-at and identical latches (latch sweep)\n" );
-    fprintf( pErr, "\t         - replaces autonomous logic by free PI variables\n" );
+//    fprintf( pErr, "\t         - replaces autonomous logic by free PI variables\n" );
     fprintf( pErr, "\t           (the latter may change sequential behaviour)\n" );
     fprintf( pErr, "\t-l     : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
-    fprintf( pErr, "\t-a     : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
+//    fprintf( pErr, "\t-a     : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -11291,9 +11401,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int nFrames;
-    int fInputs;
+    int fXInputs;
+    int fXState;
     int fVerbose;
-    extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
+    extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11301,10 +11412,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nFrames    = 10;
-    fInputs    =  0;
+    fXInputs   =  0;
+    fXState    =  0;
     fVerbose   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fisvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -11320,7 +11432,10 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
                 goto usage;
             break;
         case 'i':
-            fInputs ^= 1;
+            fXInputs ^= 1;
+            break;
+        case 's':
+            fXState ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -11343,14 +11458,15 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
+    Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
+    fprintf( pErr, "usage: xsim [-F num] [-isvh]\n" );
     fprintf( pErr, "\t         performs X-valued simulation of the AIG\n" );
     fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-i     : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
+    fprintf( pErr, "\t-i     : toggle X-valued representation of inputs [default = %s]\n", fXInputs? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle X-valued representation of state [default = %s]\n", fXState? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -11674,11 +11790,12 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     char ** pArgvNew;
     int nArgcNew;
     int c;
+    int fRetimeFirst;
     int fVerbose;
     int fVeryVerbose;
     int nFrames;
 
-    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11686,10 +11803,11 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nFrames      = 0; // if 0, iterates through frames
-    fVerbose     = 1;
+    fRetimeFirst = 1;
+    fVerbose     = 0;
     fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -11704,6 +11822,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames <= 0 ) 
                 goto usage;
             break;
+        case 'r':
+            fRetimeFirst ^= 1;
+            break;
         case 'w':
             fVeryVerbose ^= 1;
             break;
@@ -11727,18 +11848,19 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose );
+    Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs inductive sequential equivalence checking\n" );
     fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
@@ -11746,6 +11868,95 @@ usage:
     fprintf( pErr, "\t         if one file is given, uses the current network and the file\n");
     return 1;
 }
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fRetimeFirst;
+    int fVerbose;
+    int fVeryVerbose;
+    int nFrames;
+
+    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames      = 0; // if 0, iterates through frames
+    fRetimeFirst = 1;
+    fVerbose     = 0;
+    fVeryVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames <= 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            fRetimeFirst ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        printf( "The network has no latches. Used combinational command \"iprove\".\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
+    }
+
+    // perform verification
+    Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
+    fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
+    fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ce783c95..40a52ce8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -122,6 +122,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew;
     Aig_Obj_t * pObj;
     int i;
     assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
@@ -141,7 +142,19 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
+    {
+        if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
+            break;
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+    }
+    // if there are assertions, add them
+    if ( pMan->nAsserts > 0 )
+        Aig_ManForEachAssert( pMan, pObj, i )
+        {
+            pObjNew = Abc_NtkCreateAssert(pNtkNew);
+            Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
+            Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+        }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
@@ -194,7 +207,19 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachPo( pMan, pObj, i )
+    {
+        if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
+            break;
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+    }
+    // if there are assertions, add them
+    if ( pMan->nAsserts > 0 )
+        Aig_ManForEachAssert( pMan, pObj, i )
+        {
+            pObjNew = Abc_NtkCreateAssert(pNtkNew);
+            Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
+            Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+        }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
@@ -892,7 +917,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
@@ -916,7 +941,7 @@ PRT( "Initial fraiging time", clock() - clk );
     if ( pMan == NULL )
         return NULL;
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -929,6 +954,34 @@ PRT( "Initial fraiging time", clock() - clk );
 
 /**Function*************************************************************
 
+  Synopsis    [Computes latch correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL );
+    Aig_ManStop( pTemp );
+    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    else
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -938,11 +991,40 @@ PRT( "Initial fraiging time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
-    Fraig_Params_t Params;
     Aig_Man_t * pMan;
-    Abc_Ntk_t * pMiter, * pTemp;
+    int RetValue;
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+    // perform verification
+    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+{
+//    Fraig_Params_t Params;
+    Aig_Man_t * pMan;
+    Abc_Ntk_t * pMiter;//, * pTemp;
     int RetValue;
 
     // get the miter of the two networks
@@ -971,6 +1053,8 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
         return 1;
     }
 
+    // commented out because something became non-inductive
+/*
     // preprocess the miter by fraiging it
     // (note that for each functional class, fraiging leaves one representative;
     // so fraiging does not reduce the number of functions represented by nodes
@@ -978,7 +1062,25 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
     Params.nBTLimit = 100000;
     pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
     Abc_NtkDelete( pTemp );
-
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 0 )
+    {
+        extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+        // report the error
+        pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
+        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
+        FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
+        return 0;
+    }
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return 1;
+    }
+*/
     // derive the AIG manager
     pMan = Abc_NtkToDar( pMiter, 1 );
     Abc_NtkDelete( pMiter );
@@ -990,7 +1092,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
     assert( pMan->nRegs > 0 );
 
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose );
+    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -1006,15 +1108,19 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Aig_ManReduceLaches( pMan, fVerbose );
-    pMan = Aig_ManConstReduce( pMan, fVerbose );
+    Aig_ManSeqCleanup( pMan );
+    if ( fLatchSweep )
+    {
+        pMan = Aig_ManReduceLaches( pMan, fVerbose );
+        pMan = Aig_ManConstReduce( pMan, fVerbose );
+    }
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;
@@ -1038,6 +1144,8 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
         return NULL;
+//    Aig_ManReduceLachesCount( pMan );
+
     pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, 0 );
     Aig_ManStop( pTemp );
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 004d1f39..f9b053ba 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -213,6 +213,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     printf( "Total nodes = %6d   %6.2f Mb   Changes = %6d.\n", 
         s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges );
 */
+
+//    if ( Abc_NtkHasSop(pNtk) )
+//        printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 4fdb7cbc..69373597 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -233,7 +233,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
     // perform strashing
     nNewCis = 0;
     Abc_NtkCleanCopy( pNtk2 );
-    Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
+    if ( Abc_NtkIsStrash(pNtk2) )
+        Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtk1);
     Abc_NtkForEachCi( pNtk2, pObj, i )
     {
         pName = Abc_ObjName(pObj);
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index c05823da..5d9e4634 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -103,7 +103,7 @@ static inline void Abc_XsimPrint( FILE * pFile, int Value )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose )
+void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXState, int fVerbose )
 {
     Abc_Obj_t * pObj;
     int i, f;
@@ -111,20 +111,26 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
     srand( 0x12341234 );
     // start simulation
     Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
-    if ( fInputs )
+    if ( fXInputs )
     {
         Abc_NtkForEachPi( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, XVSX );
-        Abc_NtkForEachLatch( pNtk, pObj, i )
-            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
     }
     else
     {
         Abc_NtkForEachPi( pNtk, pObj, i )
             Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+    }
+    if ( fXState )
+    {
         Abc_NtkForEachLatch( pNtk, pObj, i )
             Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX );
     }
+    else
+    {
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
+    }
     // simulate and print the result
     fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" );
     for ( f = 0; f < nFrames; f++ )
@@ -147,14 +153,24 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer
         fprintf( stdout, " : " );
         Abc_NtkForEachPo( pNtk, pObj, i )
             Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+        if ( Abc_NtkAssertNum(pNtk) )
+        {
+        fprintf( stdout, " : " );
+        Abc_NtkForEachAssert( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+        }
         fprintf( stdout, "\n" );
         // assign input values
-        if ( fInputs )
+        if ( fXInputs )
+        {
             Abc_NtkForEachPi( pNtk, pObj, i )
                 Abc_ObjSetXsim( pObj, XVSX );
+        }
         else
+        {
             Abc_NtkForEachPi( pNtk, pObj, i )
                 Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+        }
         // transfer the latch values
         Abc_NtkForEachLatch( pNtk, pObj, i )
             Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
diff --git a/src/opt/fxu/fxu.c b/src/opt/fxu/fxu.c
index a92ef934..d11fd793 100644
--- a/src/opt/fxu/fxu.c
+++ b/src/opt/fxu/fxu.c
@@ -58,6 +58,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
     Fxu_Single * pSingle;
     Fxu_Double * pDouble;
     int Weight1, Weight2, Weight3;
+    int Counter = 0;
 
     s_MemoryTotal = 0;
     s_MemoryPeak  = 0;
@@ -77,7 +78,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
         {
             Weight1 = Fxu_HeapSingleReadMaxWeight( p->pHeapSingle );
             if ( pData->fVerbose )
-                printf( "Best single = %3d.\n", Weight1 );
+                printf( "Div %5d : Best single = %5d.\r", Counter++, Weight1 );
             if ( Weight1 > 0 || Weight1 == 0 && pData->fUse0 )
                 Fxu_UpdateSingle( p );
             else
@@ -92,7 +93,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
         {
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
             if ( pData->fVerbose )
-                printf( "Best double = %3d.\n", Weight2 );
+                printf( "Div %5d : Best double = %5d.\r", Counter++, Weight2 );
             if ( Weight2 > 0 || Weight2 == 0 && pData->fUse0 )
                 Fxu_UpdateDouble( p );
             else
@@ -109,7 +110,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             Weight2 = Fxu_HeapDoubleReadMaxWeight( p->pHeapDouble );
 
             if ( pData->fVerbose )
-                printf( "Best double = %3d. Best single = %3d.\n", Weight2, Weight1 );
+                printf( "Div %5d : Best double = %5d. Best single = %5d.\r", Counter++, Weight2, Weight1 );
 //Fxu_Select( p, &pSingle, &pDouble );
 
             if ( Weight1 >= Weight2 )
@@ -140,8 +141,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
             // select the best single and double
             Weight3 = Fxu_Select( p, &pSingle, &pDouble );
             if ( pData->fVerbose )
-                printf( "Best double = %3d. Best single = %3d. Best complement = %3d.\n", 
-                    Weight2, Weight1, Weight3 );
+                printf( "Div %5d : Best double = %5d. Best single = %5d. Best complement = %5d.\r", 
+                    Counter++, Weight2, Weight1, Weight3 );
 
             if ( Weight3 > 0 || Weight3 == 0 && pData->fUse0 )
                 Fxu_Update( p, pSingle, pDouble );
@@ -152,7 +153,8 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
     }
 
     if ( pData->fVerbose )
-        printf( "Total single = %3d. Total double = %3d. Total compl = %3d.\n", p->nDivs1, p->nDivs2, p->nDivs3 );
+        printf( "Total single = %3d. Total double = %3d. Total compl = %3d.                    \n", 
+        p->nDivs1, p->nDivs2, p->nDivs3 );
 
     // create the new covers
     if ( pData->nNodesNew )
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 7025d019..e6d0b69e 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -55,7 +55,8 @@ struct FxuDataStruct
     bool              fUseCompl;        // set to 1 to have complement taken into account
     bool              fVerbose;         // set to 1 to have verbose output
     int               nNodesExt;        // the number of divisors to extract
-    int               nPairsMax;        // the maximum number of cube pairs to consider
+    int               nSingleMax;       // the max number of single-cube divisors to consider
+    int               nPairsMax;        // the max number of double-cube divisors to consider
     // the input information
     Vec_Ptr_t *       vSops;            // the SOPs for each node in the network
     Vec_Ptr_t *       vFanins;          // the fanins of each node in the network
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 99942a88..e3300df9 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -178,12 +178,26 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
 
     // consider the case when cube pairs should be preprocessed
     // before adding them to the set of divisors
+//    if ( pData->fVerbose )
+//        printf( "The total number of cube pairs is %d.\n", nPairsTotal );
+    if ( nPairsTotal > 10000000 )
+    {
+        printf( "The total number of cube pairs of the network is more than 10,000,000.\n" );
+        printf( "Command \"fx\" takes a long time to run in such cases. It is suggested\n" );
+        printf( "that the user changes the network by reducing the size of logic node and\n" );
+        printf( "consequently the number of cube pairs to be processed by this command.\n" );
+        printf( "One way to achieve this is to run the commands \"st; multi -m -F <num>\"\n" );
+        printf( "as a proprocessing step, while selecting <num> as approapriate.\n" );
+        return NULL;
+    }
     if ( nPairsTotal > pData->nPairsMax )
         if ( !Fxu_PreprocessCubePairs( p, pData->vSops, nPairsTotal, pData->nPairsMax ) )
             return NULL;
+//    if ( pData->fVerbose )
+//        printf( "Only %d best cube pairs will be used by the fast extract command.\n", pData->nPairsMax );
 
     // add the var pairs to the heap
-    Fxu_MatrixComputeSingles( p );
+    Fxu_MatrixComputeSingles( p, pData->fUse0, pData->nSingleMax );
 
     // print stats
     if ( pData->fVerbose )
@@ -194,9 +208,8 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
             p->lVars.nItems, p->lCubes.nItems );
         fprintf( stdout, "Lits = %d  Density = %.5f%%\n", 
             p->nEntries, Density );
-        fprintf( stdout, "1-cube divisors = %6d.  ",  p->lSingles.nItems );
-        fprintf( stdout, "2-cube divisors = %6d.  ",  p->nDivsTotal );
-        fprintf( stdout, "Cube pairs = %6d.",    nPairsTotal );
+        fprintf( stdout, "1-cube divs = %6d. (Total = %6d)  ",  p->lSingles.nItems, p->nSingleTotal );
+        fprintf( stdout, "2-cube divs = %6d. (Total = %6d)",  p->nDivsTotal, nPairsTotal );
         fprintf( stdout, "\n" );
     }
 //    Fxu_MatrixPrint( stdout, p );
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 0ae1d79e..ea85cb79 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -172,6 +172,8 @@ struct FxuMatrix // ~ 30 words
     // the single cube divisors
     Fxu_ListSingle   lSingles;    // the linked list of single cube divisors  
     Fxu_HeapSingle * pHeapSingle; // the heap of variables by the number of literals in the matrix
+    int              nWeightLimit;// the limit on weight of single cube divisors collected
+    int              nSingleTotal;// the total number of single cube divisors
     // storage for cube pairs
     Fxu_Pair ***     pppPairs;
     Fxu_Pair **      ppPairs;
@@ -459,7 +461,7 @@ extern void         Fxu_PairClearStorage( Fxu_Cube * pCube );
 extern Fxu_Pair *   Fxu_PairAlloc( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2 );
 extern void         Fxu_PairAdd( Fxu_Pair * pPair );
 /*===== fxuSingle.c ====================================================*/
-extern void         Fxu_MatrixComputeSingles( Fxu_Matrix * p );
+extern void         Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax );
 extern void         Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar );
 extern int          Fxu_SingleCountCoincidence( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVar2 );
 /*===== fxuMatrix.c ====================================================*/
diff --git a/src/opt/fxu/fxuSingle.c b/src/opt/fxu/fxuSingle.c
index be90e159..73d9a76c 100644
--- a/src/opt/fxu/fxuSingle.c
+++ b/src/opt/fxu/fxuSingle.c
@@ -17,11 +17,14 @@
 ***********************************************************************/
 
 #include "fxuInt.h"
+#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -38,12 +41,130 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
+void Fxu_MatrixComputeSingles( Fxu_Matrix * p, int fUse0, int nSingleMax )
 {
     Fxu_Var * pVar;
-    // iterate through the columns in the matrix
+    Vec_Ptr_t * vSingles;
+    int i, k;
+    // set the weight limit
+    p->nWeightLimit = 1 - fUse0;
+    // iterate through columns in the matrix and collect single-cube divisors
+    vSingles = Vec_PtrAlloc( 10000 );
     Fxu_MatrixForEachVariable( p, pVar )
-        Fxu_MatrixComputeSinglesOne( p, pVar );
+        Fxu_MatrixComputeSinglesOneCollect( p, pVar, vSingles );
+    p->nSingleTotal = Vec_PtrSize(vSingles) / 3;
+    // check if divisors should be filtered
+    if ( Vec_PtrSize(vSingles) > nSingleMax )
+    {
+        int * pWeigtCounts, nDivCount, Weight, i, c;;
+        assert( Vec_PtrSize(vSingles) % 3 == 0 );
+        // count how many divisors have the given weight
+        pWeigtCounts = ALLOC( int, 1000 );
+        memset( pWeigtCounts, 0, sizeof(int) * 1000 );
+        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
+        {
+            Weight = (int)Vec_PtrEntry(vSingles, i);
+            if ( Weight >= 999 )
+                pWeigtCounts[999]++;
+            else
+                pWeigtCounts[Weight]++;
+        }
+        // select the bound on the weight (above this bound, singles will be included)
+        nDivCount = 0;
+        for ( c = 999; c >= 0; c-- )
+        {
+            nDivCount += pWeigtCounts[c];
+            if ( nDivCount >= nSingleMax )
+                break;
+        }
+        free( pWeigtCounts );
+        // collect singles with the given costs
+        k = 0;
+        for ( i = 2; i < Vec_PtrSize(vSingles); i += 3 )
+        {
+            Weight = (int)Vec_PtrEntry(vSingles, i);
+            if ( Weight < c )
+                continue;
+            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-2) );
+            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i-1) );
+            Vec_PtrWriteEntry( vSingles, k++, Vec_PtrEntry(vSingles, i) );
+            if ( k/3 == nSingleMax )
+                break;
+        }
+        Vec_PtrShrink( vSingles, k );
+        // adjust the weight limit
+        p->nWeightLimit = c;
+    }
+    // collect the selected divisors
+    assert( Vec_PtrSize(vSingles) % 3 == 0 );
+    for ( i = 0; i < Vec_PtrSize(vSingles); i += 3 )
+    {
+        Fxu_MatrixAddSingle( p, 
+            Vec_PtrEntry(vSingles,i), 
+            Vec_PtrEntry(vSingles,i+1), 
+            (int)Vec_PtrEntry(vSingles,i+2) );
+    }
+    Vec_PtrFree( vSingles );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the single-cube divisors associated with a new column.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fxu_MatrixComputeSinglesOneCollect( Fxu_Matrix * p, Fxu_Var * pVar, Vec_Ptr_t * vSingles )
+{
+    Fxu_Lit * pLitV, * pLitH;
+    Fxu_Var * pVar2;
+    int Coin;
+    int WeightCur;
+
+    // start collecting the affected vars
+    Fxu_MatrixRingVarsStart( p );
+    // go through all the literals of this variable
+    for ( pLitV = pVar->lLits.pHead; pLitV; pLitV = pLitV->pVNext )
+        // for this literal, go through all the horizontal literals
+        for ( pLitH = pLitV->pHPrev; pLitH; pLitH = pLitH->pHPrev )
+        {
+            // get another variable
+            pVar2 = pLitH->pVar;
+            // skip the var if it is already used
+            if ( pVar2->pOrder )
+                continue;
+            // skip the var if it belongs to the same node
+//            if ( pValue2Node[pVar->iVar] == pValue2Node[pVar2->iVar] )
+//                continue;
+            // collect the var
+            Fxu_MatrixRingVarsAdd( p, pVar2 );
+        }
+    // stop collecting the selected vars
+    Fxu_MatrixRingVarsStop( p );
+
+    // iterate through the selected vars
+    Fxu_MatrixForEachVarInRing( p, pVar2 )
+    {
+        // count the coincidence
+        Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
+        assert( Coin > 0 );
+        // get the new weight
+        WeightCur = Coin - 2;
+        // peformance fix (August 24, 2007)
+        if ( WeightCur >= p->nWeightLimit )
+        {
+            Vec_PtrPush( vSingles, pVar2 );
+            Vec_PtrPush( vSingles, pVar );
+            Vec_PtrPush( vSingles, (void *)WeightCur );
+        }
+    }
+
+    // unmark the vars
+    Fxu_MatrixRingVarsUnmark( p );
 }
 
 /**Function*************************************************************
@@ -59,12 +180,9 @@ void Fxu_MatrixComputeSingles( Fxu_Matrix * p )
 ***********************************************************************/
 void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
 {
-//    int * pValue2Node = p->pValue2Node;
     Fxu_Lit * pLitV, * pLitH;
     Fxu_Var * pVar2;
     int Coin;
-//    int CounterAll;
-//    int CounterTest;
     int WeightCur;
 
     // start collecting the affected vars
@@ -76,7 +194,6 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
         {
             // get another variable
             pVar2 = pLitH->pVar;
-//            CounterAll++;
             // skip the var if it is already used
             if ( pVar2->pOrder )
                 continue;
@@ -92,16 +209,17 @@ void Fxu_MatrixComputeSinglesOne( Fxu_Matrix * p, Fxu_Var * pVar )
     // iterate through the selected vars
     Fxu_MatrixForEachVarInRing( p, pVar2 )
     {
-//        CounterTest++;
         // count the coincidence
         Coin = Fxu_SingleCountCoincidence( p, pVar2, pVar );
         assert( Coin > 0 );
         // get the new weight
         WeightCur = Coin - 2;
-        if ( WeightCur >= 0 )
+        // peformance fix (August 24, 2007)
+//        if ( WeightCur >= 0 )
+//        Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
+        if ( WeightCur >= p->nWeightLimit )
             Fxu_MatrixAddSingle( p, pVar2, pVar, WeightCur );
     }
-
     // unmark the vars
     Fxu_MatrixRingVarsUnmark( p );
 }
diff --git a/src/opt/fxu/fxuUpdate.c b/src/opt/fxu/fxuUpdate.c
index a430b9c1..274f79f6 100644
--- a/src/opt/fxu/fxuUpdate.c
+++ b/src/opt/fxu/fxuUpdate.c
@@ -757,12 +757,14 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
 { 
     Fxu_Single * pSingle, * pSingle2;
     int WeightNew;
+    int Counter = 0;
 
     Fxu_MatrixForEachSingleSafe( p, pSingle, pSingle2 )
     {
         // if at least one of the variables is marked, recalculate
         if ( pSingle->pVar1->pOrder || pSingle->pVar2->pOrder )
         {
+            Counter++;
             // get the new weight
             WeightNew = -2 + Fxu_SingleCountCoincidence( p, pSingle->pVar1, pSingle->pVar2 );
             if ( WeightNew >= 0 )
@@ -778,6 +780,7 @@ void Fxu_UpdateCleanOldSingles( Fxu_Matrix * p )
             }
         }
     }
+//    printf( "Called procedure %d times.\n", Counter );
 }
 
 /**Function*************************************************************