Version abc70818

11 files changed, 911 insertions, 916 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 1051aa30..2bb19a34 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -49,8 +49,9 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Fra_Par_t_   Fra_Par_t;
-typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
+typedef struct Fra_Cla_t_   Fra_Cla_t;
+typedef struct Fra_Sml_t_   Fra_Sml_t;
 
 // FRAIG parameters
 struct Fra_Par_t_
@@ -72,6 +73,7 @@ struct Fra_Par_t_
     int              nFramesK;          // the number of timeframes to unroll
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
+    int              fUseImps;          // use implications
 };
 
 // FRAIG equivalence classes
@@ -88,6 +90,19 @@ struct Fra_Cla_t_
     Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
     int              nPairs;            // the number of pairs of nodes
     int              fRefinement;       // set to 1 when refinement has happened
+    Vec_Int_t *      vImps;             // implications
+};
+
+// simulation manager
+struct Fra_Sml_t_
+{
+    Aig_Man_t *      pAig;              // the original AIG manager
+    int              nFrames;           // the number of times frames
+    int              nWordsFrame;       // the number of words in each time frame
+    int              nWordsTotal;       // the total number of words at a node
+    int              nSimRounds;        // statistics
+    int              timeSim;           // statistics
+    unsigned         pData[0];          // simulation data for the nodes
 };
 
 // FRAIG manager
@@ -101,17 +116,14 @@ struct Fra_Man_t_
     // mapping AIG into FRAIG
     int              nFramesAll;        // the number of timeframes used
     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
+    // equivalence classes 
+    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
     // simulation info
-    void *           pSim;              // the simulation manager
-    unsigned *       pSimWords;         // memory for simulation information
-    int              nSimWords;         // the number of simulation words
+    Fra_Sml_t *      pSml;              // simulation manager
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
-    int *            pPatScores;        // the scores of each pattern
-    // equivalence classes 
-    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
-    // equivalence checking
+    // satisfiability solving
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
     Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
@@ -140,6 +152,8 @@ struct Fra_Man_t_
     int              nSpeculs;   
     int              nChoices;
     int              nChoicesFake;
+    int              nSatCallsRecent;
+    int              nSatCallsSkipped;
     // runtime
     int              timeSim;
     int              timeTrav;
@@ -158,8 +172,8 @@ struct Fra_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;   }
-static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
+static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
+static inline unsigned     Fra_ObjRandomSim()                                            { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
 
 static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
 static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
@@ -196,6 +210,7 @@ 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 );
 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
+extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
@@ -203,9 +218,14 @@ extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pP
 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 );
-/*=== fraDfs.c ========================================================*/
+/*=== 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 );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -217,6 +237,7 @@ extern void                Fra_ManStop( Fra_Man_t * p );
 extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
 extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+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 );
@@ -224,10 +245,15 @@ extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbos
 extern int                 Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
 extern int                 Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern unsigned            Fra_NodeHashSims( Aig_Obj_t * pObj );
-extern void                Fra_SavePattern( Fra_Man_t * p );
-extern void                Fra_Simulate( Fra_Man_t * p, int fInit );
-extern void                Fra_Resimulate( Fra_Man_t * p );
 extern int                 Fra_CheckOutputSims( Fra_Man_t * p );
+extern void                Fra_SavePattern( Fra_Man_t * p );
+extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
+extern void                Fra_SmlResimulate( Fra_Man_t * p );
+extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame );
+extern void                Fra_SmlStop( Fra_Sml_t * p );
+extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords );
+extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
+
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 8923c7b0..9c10ae3b 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -90,6 +90,7 @@ void Fra_ClassesStop( Fra_Cla_t * p )
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
     if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
     if ( p->vClasses )     Vec_PtrFree( p->vClasses );
+    if ( p->vImps )        Vec_IntFree( p->vImps );
     free( p );
 }
 
@@ -597,6 +598,93 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p )
     p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1s in the XOR of simulation data.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
+{
+    unsigned * pSimL, * pSimR;
+    int k, Counter = 0;
+    pSimL = Fra_ObjSim( p, Left );
+    pSimR = Fra_ObjSim( p, Right );
+    for ( k = 0; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Postprocesses the classes by removing half of the less useful.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesPostprocess( Fra_Cla_t * p )
+{
+    int Ratio = 2;
+    Fra_Sml_t * pComb;
+    Aig_Obj_t * pObj, * pRepr, ** ppClass;
+    int * pWeights, WeightMax = 0, i, k, c;
+    // perform combinational simulation
+    pComb = Fra_SmlSimulateComb( p->pAig, 32 );
+    // compute the weight of each node in the classes
+    pWeights = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
+    memset( pWeights, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    { 
+        pRepr = Fra_ClassObjRepr( pObj );
+        if ( pRepr == NULL )
+            continue;
+        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
+        WeightMax = AIG_MAX( WeightMax, pWeights[i] );
+    }
+    Fra_SmlStop( pComb );
+    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
+    // remove nodes from classes whose weight is less than WeightMax/Ratio
+    k = 0;
+    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+    {
+        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
+            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
+        else
+            Fra_ClassObjSetRepr( pObj, NULL );
+    }
+    Vec_PtrShrink( p->vClasses1, k );
+    // in each class, compact the nodes
+    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
+    {
+        k = 1;
+        for ( c = 1; ppClass[c]; c++ )
+        {
+            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
+                ppClass[k++] = ppClass[c];
+            else
+                Fra_ClassObjSetRepr( ppClass[c], NULL );
+        }
+        ppClass[k] = NULL;
+    }
+    // remove classes with only repr
+    k = 0;
+    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
+        if ( ppClass[1] != NULL )
+            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
+    Vec_PtrShrink( p->vClasses, k );
+    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
+    free( pWeights );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 41d264bb..f28793aa 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -142,7 +142,10 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
     pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+    {
+        p->nSatCallsSkipped++;
         return;
+    }
     assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
     // if they are proved different, the c-ex will be in p->pPatWords
     RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@@ -177,7 +180,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
     if ( p->vTimeouts )
         Vec_PtrPush( p->vTimeouts, pObj );
     // simulate the counter-example and return the Fraig node
-    Fra_Resimulate( p );
+    Fra_SmlResimulate( p );
     if ( Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
@@ -198,13 +201,18 @@ void Fra_FraigSweep( Fra_Man_t * p )
 {
     ProgressBar * pProgress;
     Aig_Obj_t * pObj, * pObjNew;
-    int i, k = 0;
-    // duplicate internal nodes
-    pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
+    int i, k = 0, Pos = 0;
     // fraig latch outputs
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+    {
         Fra_FraigNode( p, pObj );
+        if ( p->pPars->fUseImps )
+            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
+    }
+    if ( p->pPars->fLatchCorr )
+        return;
     // fraig internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
     Aig_ManForEachNode( p->pManAig, pObj, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
@@ -217,6 +225,8 @@ void Fra_FraigSweep( Fra_Man_t * p )
             continue;
         // perform fraiging
         Fra_FraigNode( p, pObj );
+        if ( p->pPars->fUseImps )
+            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
     }
     Extra_ProgressBarStop( pProgress );
     // try to prove the outputs of the miter
@@ -224,6 +234,9 @@ void Fra_FraigSweep( Fra_Man_t * p )
 //    Fra_MiterStatus( p->pManFraig );
 //    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
 //        Fra_MiterProve( p );
+    // compress implications after processing all of them
+    if ( p->pPars->fUseImps )
+        Fra_ImpCompactArray( p->pCla->vImps );
 }
 
 /**Function*************************************************************
@@ -248,7 +261,8 @@ clk = clock();
     assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
-    Fra_Simulate( p, 0 );
+    p->pSml = Fra_SmlStart( pManAig, 1, pPars->nSimWords );
+    Fra_SmlSimulate( p, 0 );
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
     // collect initial states
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 9643b887..d5761fbe 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -24,23 +24,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// simulation manager
-typedef struct Sml_Man_t_   Sml_Man_t;
-struct Sml_Man_t_
-{
-    Aig_Man_t *      pAig;
-    int              nFrames;
-    int              nWordsFrame;
-    int              nWordsTotal;
-    unsigned         pData[0];
-};
-
-static inline unsigned * Sml_ObjSim( Sml_Man_t * p, int Id )  { return p->pData + p->nWordsTotal * Id; }
-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;           }
-
-static int * s_ImpCost = NULL;
+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                         ///
@@ -48,377 +34,6 @@ static int * s_ImpCost = NULL;
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sml_Man_t * Sml_ManStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame )
-{
-    Sml_Man_t * p;
-    assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
-    p = (Sml_Man_t *)malloc( sizeof(Sml_Man_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame );
-    memset( p, 0, sizeof(Sml_Man_t) + sizeof(unsigned) * nFrames * nWordsFrame );
-    p->nFrames     = nFrames;
-    p->nWordsFrame = nWordsFrame;
-    p->nWordsTotal = nFrames * nWordsFrame;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_ManStop( Sml_Man_t * p )
-{
-    free( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Assigns random patterns to the PI node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_ManAssignRandom( Sml_Man_t * p, Aig_Obj_t * pObj )
-{
-    unsigned * pSims;
-    int i;
-    assert( Aig_ObjIsPi(pObj) );
-    pSims = Sml_ObjSim( p, pObj->Id );
-    for ( i = 0; i < p->nWordsTotal; i++ )
-        pSims[i] = Fra_ObjRandomSim();
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assigns constant patterns to the PI node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_ManAssignConst( Sml_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
-{
-    unsigned * pSims;
-    int i;
-    assert( Aig_ObjIsPi(pObj) );
-    pSims = Sml_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
-    for ( i = 0; i < p->nWordsFrame; i++ )
-        pSims[i] = fConst1? ~(unsigned)0 : 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assings random simulation info for the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_ManInitialize( Sml_Man_t * p, int fInit )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    if ( fInit )
-    {
-        assert( Aig_ManRegNum(p->pAig) > 0 );
-        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
-        // assign random info for primary inputs
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Sml_ManAssignRandom( p, pObj );
-        // assign the initial state for the latches
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Sml_ManAssignConst( p, pObj, 0, 0 );
-    }
-    else
-    {
-        Aig_ManForEachPi( p->pAig, pObj, i )
-            Sml_ManAssignRandom( p, pObj );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assings distance-1 simulation info for the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_ManAssignDist1( Sml_Man_t * p, unsigned * pPat )
-{
-    Aig_Obj_t * pObj;
-    int f, i, k, Limit, nTruePis;
-    assert( p->nFrames > 0 );
-    if ( p->nFrames == 1 )
-    {
-        // copy the PI info 
-        Aig_ManForEachPi( p->pAig, pObj, i )
-            Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
-        // flip one bit
-        Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
-        for ( i = 0; i < Limit; i++ )
-            Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
-    }
-    else
-    {
-        // copy the PI info for each frame
-        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
-        for ( f = 0; f < p->nFrames; f++ )
-            Aig_ManForEachPiSeq( p->pAig, pObj, i )
-                Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
-        // copy the latch info 
-        k = 0;
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
-//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
-
-        // flip one bit of the last frame
-        if ( p->nFrames == 2 )
-        {
-            Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
-            for ( i = 0; i < Limit; i++ )
-                Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
-//            Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_NodeSimulate( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pSims, * pSims0, * pSims1;
-    int fCompl, fCompl0, fCompl1, i;
-    int nSimWords = p->nWordsFrame;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    assert( iFrame == 0 || nSimWords < p->nWordsTotal );
-    // get hold of the simulation information
-    pSims  = Fra_ObjSim(pObj) + nSimWords * iFrame;
-    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
-    pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
-    // get complemented attributes of the children using their random info
-    fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
-    fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
-    // simulate
-    if ( fCompl0 && fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = (pSims0[i] | pSims1[i]);
-        else
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = ~(pSims0[i] | pSims1[i]);
-    }
-    else if ( fCompl0 && !fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = (pSims0[i] | ~pSims1[i]);
-        else
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = (~pSims0[i] & pSims1[i]);
-    }
-    else if ( !fCompl0 && fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = (~pSims0[i] | pSims1[i]);
-        else
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = (pSims0[i] & ~pSims1[i]);
-    }
-    else // if ( !fCompl0 && !fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = ~(pSims0[i] & pSims1[i]);
-        else
-            for ( i = 0; i < nSimWords; i++ )
-                pSims[i] = (pSims0[i] & pSims1[i]);
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_NodeCopyFanin( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pSims, * pSims0;
-    int fCompl, fCompl0, i;
-    int nSimWords = p->nWordsFrame;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsPo(pObj) );
-    assert( iFrame == 0 || nSimWords < p->nWordsTotal );
-    // get hold of the simulation information
-    pSims  = Sml_ObjSim(p, pObj->Id) + nSimWords * iFrame;
-    pSims0 = Sml_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + nSimWords * iFrame;
-    // get complemented attributes of the children using their random info
-    fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
-    // copy information as it is
-    if ( fCompl0 )
-        for ( i = 0; i < nSimWords; i++ )
-            pSims[i] = ~pSims0[i];
-    else
-        for ( i = 0; i < nSimWords; i++ )
-            pSims[i] = pSims0[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_NodeTransferNext( Sml_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
-{
-    unsigned * pSims0, * pSims1;
-    int i, nSimWords = p->nWordsFrame;
-    assert( !Aig_IsComplement(pOut) );
-    assert( !Aig_IsComplement(pIn) );
-    assert( Aig_ObjIsPo(pOut) );
-    assert( Aig_ObjIsPi(pIn) );
-    assert( iFrame == 0 || nSimWords < p->nWordsTotal );
-    // get hold of the simulation information
-    pSims0 = Sml_ObjSim(p, pOut->Id) + nSimWords * iFrame;
-    pSims1 = Sml_ObjSim(p, pIn->Id) + nSimWords * (iFrame+1);
-    // copy information as it is
-    for ( i = 0; i < nSimWords; i++ )
-        pSims1[i] = pSims0[i];
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates AIG manager.]
-
-  Description [Assumes that the PI simulation info is attached.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sml_SimulateOne( Sml_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int f, i, clk;
-clk = clock();
-    for ( f = 0; f < p->nFrames; f++ )
-    {
-        // simulate the nodes
-        Aig_ManForEachNode( p->pAig, pObj, i )
-            Sml_NodeSimulate( p, pObj, f );
-        if ( f == p->nFrames - 1 )
-            break;
-        // copy simulation info into outputs
-        Aig_ManForEachLiSeq( p->pAig, pObj, i )
-            Sml_NodeCopyFanin( p, pObj, f );
-        // copy simulation info into the inputs
-//        for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
-//            Sml_NodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
-        Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
-            Sml_NodeTransferNext( p, pObjLi, pObjLo, f );
-    }
-//p->timeSim += clock() - clk;
-//p->nSimRounds++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs simulation of the uninitialized circuit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sml_Man_t * Sml_ManSimulateComb( Aig_Man_t * pAig, int nWords )
-{
-    Sml_Man_t * p;
-    p = Sml_ManStart( pAig, 1, nWords );
-    Sml_ManInitialize( p, 0 );
-    Sml_SimulateOne( p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs simulation of the initialized circuit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Sml_Man_t * Sml_ManSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
-{
-    Sml_Man_t * p;
-    p = Sml_ManStart( pAig, nFrames, nWords );
-    Sml_ManInitialize( p, 1 );
-    Sml_SimulateOne( p );
-    return p;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Counts the number of 1s in each siminfo of each node.]
 
   Description []
@@ -428,16 +43,16 @@ Sml_Man_t * Sml_ManSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-int * Sml_ManCountOnes( Sml_Man_t * p )
+static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj;
     unsigned * pSim;
     int i, k, * pnBits; 
     pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );  
-    memset( pnBits, 0, sizeof(int) * Aig_ManObjIdMax(p->pAig) + 1 );
+    memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        pSim = Sml_ObjSim( p, i );
+        pSim = Fra_ObjSim( p, i );
         for ( k = 0; k < p->nWordsTotal; k++ )
             pnBits[i] += Aig_WordCountOnes( pSim[k] );
     }
@@ -455,12 +70,12 @@ int * Sml_ManCountOnes( Sml_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sml_NodeNotImpCost( Sml_Man_t * p, int Left, int Right )
+static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
 {
     unsigned * pSimL, * pSimR;
     int k, Counter = 0;
-    pSimL = Sml_ObjSim( p, Left );
-    pSimR = Sml_ObjSim( p, Right );
+    pSimL = Fra_ObjSim( p, Left );
+    pSimR = Fra_ObjSim( p, Right );
     for ( k = 0; k < p->nWordsTotal; k++ )
         Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
     return Counter;
@@ -477,12 +92,12 @@ static inline int Sml_NodeNotImpCost( Sml_Man_t * p, int Left, int Right )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sml_NodeCheckImp( Sml_Man_t * p, int Left, int Right )
+static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
 {
     unsigned * pSimL, * pSimR;
     int k;
-    pSimL = Sml_ObjSim( p, Left );
-    pSimR = Sml_ObjSim( p, Right );
+    pSimL = Fra_ObjSim( p, Left );
+    pSimR = Fra_ObjSim( p, Right );
     for ( k = 0; k < p->nWordsTotal; k++ )
         if ( pSimL[k] & ~pSimR[k] )
             return 0;
@@ -500,42 +115,69 @@ static inline int Sml_NodeCheckImp( Sml_Man_t * p, int Left, int Right )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p )
+Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
 {
     Aig_Obj_t * pObj;
     Vec_Ptr_t * vNodes;
     int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
+    assert( p->nWordsTotal > 0 );
     // count 1s in each node's siminfo
-    pnBits = Sml_ManCountOnes( p );
+    pnBits = Fra_SmlCountOnes( p );
     // count number of nodes having that many 1s
-    nBits = p->nWordsTotal * 32;
-    assert( nBits >= 32 );
     nNodes = 0;
-    pnNodes = ALLOC( int, nBits );
-    memset( pnNodes, 0, sizeof(int) * nBits );
+    nBits = p->nWordsTotal * 32;
+    pnNodes = ALLOC( int, nBits + 1 );
+    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
         if ( i == 0 ) continue;
-        assert( pnBits[i] < nBits ); // "<" because of normalized info
+        // skip non-PI and non-internal nodes
+        if ( fLatchCorr )
+        {
+            if ( !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        else
+        {
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        // skip nodes participating in the classes
+//        if ( Fra_ClassObjRepr(pObj) )
+//            continue;
+        assert( pnBits[i] <= nBits ); // "<" because of normalized info
         pnNodes[pnBits[i]]++;
         nNodes++;
     }
     // allocate memory for all the nodes
-    pMemory = ALLOC( int, nNodes + nBits );  
+    pMemory = ALLOC( int, nNodes + nBits + 1 );  
     // markup the memory for each node
-    vNodes = Vec_PtrAlloc( nBits );
+    vNodes = Vec_PtrAlloc( nBits + 1 );
     Vec_PtrPush( vNodes, pMemory );
-    Aig_ManForEachObj( p->pAig, pObj, i )
+    for ( i = 1; i <= nBits; i++ )
     {
-        if ( i == 0 ) continue;
-        pMemory += pnBits[i-1] + 1;
+        pMemory += pnNodes[i-1] + 1;
         Vec_PtrPush( vNodes, pMemory );
     }
     // add the nodes
-    memset( pnNodes, 0, sizeof(int) * nBits );
+    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
         if ( i == 0 ) continue;
+        // skip non-PI and non-internal nodes
+        if ( fLatchCorr )
+        {
+            if ( !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        else
+        {
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        // skip nodes participating in the classes
+//        if ( Fra_ClassObjRepr(pObj) )
+//            continue;
         pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
         pMemory[ pnNodes[pnBits[i]]++ ] = i;
     }
@@ -546,13 +188,15 @@ Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p )
         pMemory[ pnNodes[i]++ ] = 0;
         nTotal += pnNodes[i];
     }
-    assert( nTotal == nNodes + nBits );
+    assert( nTotal == nNodes + nBits + 1 );
+    free( pnNodes );
+    free( pnBits );
     return vNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Compares two implications using their cost.]
+  Synopsis    [Returns the array of implications with the highest cost.]
 
   Description []
                
@@ -561,15 +205,41 @@ Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Sml_CompareCost( int * pNum1, int * pNum2 )
+Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit )
 {
-    int Cost1 = s_ImpCost[*pNum1];
-    int Cost2 = s_ImpCost[*pNum2];
-    if ( Cost1 > Cost2 )
-        return -1;
-    if ( Cost1 < Cost2  )
-        return 1;
-    return 0; 
+    Vec_Int_t * vImpsNew;
+    int * pCostCount, nImpCount, Imp, i, c;
+    assert( Vec_IntSize(vImps) >= nImpLimit );
+    // count how many implications have each cost
+    pCostCount = ALLOC( int, nCostMax + 1 );
+    memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
+    for ( i = 0; i < Vec_IntSize(vImps); i++ )
+    {
+        assert( pCosts[i] <= nCostMax );
+        pCostCount[ pCosts[i] ]++;
+    }
+    assert( pCostCount[0] == 0 );
+    // select the bound on the cost (above this bound, implication will be included)
+    nImpCount = 0;
+    for ( c = nCostMax; c > 0; c-- )
+    {
+        nImpCount += pCostCount[c];
+        if ( nImpCount >= nImpLimit )
+            break;
+    }
+//    printf( "Cost range >= %d.\n", c );
+    // collect implications with the given costs
+    vImpsNew = Vec_IntAlloc( nImpLimit );
+    Vec_IntForEachEntry( vImps, Imp, i )
+    {
+        if ( pCosts[i] < c )
+            continue;
+        Vec_IntPush( vImpsNew, Imp );
+        if ( Vec_IntSize( vImpsNew ) == nImpLimit )
+            break;
+    }
+    free( pCostCount );
+    return vImpsNew;
 }
 
 /**Function*************************************************************
@@ -602,72 +272,103 @@ int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
   (1) they hold using sequential simulation information
   (2) they do not hold using combinational simulation information
   (3) they have as high expressive power as possible (heuristically)
-      - this means they are relatively far in terms of Humming distance
-        meaning their complement covers a larger Boolean space
-      - they are easy to disprove combinationally
-        meaning they cover relatively a larger sequential subspace.]
+      that is, they are easy to disprove combinationally
+      meaning they cover relatively larger sequential subspace.]
                
-  SideEffects [The managers should have the first pattern (000...)]
+  SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sml_ManImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit )
+Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
 {
-    Sml_Man_t * pSeq, * pComb;
+//    Aig_Obj_t * pObj;
+    int nSimWords = 64;
+    Fra_Sml_t * pSeq, * pComb;
     Vec_Int_t * vImps, * vTemp;
     Vec_Ptr_t * vNodes;
-    int * pNodesI, * pNodesK, * pNumbers;
-    int i, k, Imp;
+    int * pImpCosts, * pNodesI, * pNodesK;
+    int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
+    int CostMin = AIG_INFINITY, CostMax = 0;
+    int i, k, Imp, clk = clock();
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
-    pComb = Sml_ManSimulateComb( p->pManAig, 32 );
-    pSeq = Sml_ManSimulateSeq( p->pManAig, 32, 1 );
+    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, nSimWords, 1 );
     // get the nodes sorted by the number of 1s
-    vNodes = Sml_ManSortUsingOnes( pSeq );
+    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-- )
+    for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+    for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+        nImpsTotal++;
+
     // compute implications and their costs
-    s_ImpCost = ALLOC( int, nImpMaxLimit );
+    pImpCosts = ALLOC( int, nImpMaxLimit );
     vImps = Vec_IntAlloc( nImpMaxLimit );
-    for ( k = pSeq->nWordsTotal * 32 - 1; k >= 0; k-- )
-        for ( i = k - 1; i >= 0; i-- )
+    for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
+        for ( i = k - 1; i > 0; i-- )
         {
             for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
             for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
             {
-                if ( Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) &&
-                    !Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
+                nImpsTried++;
+                if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
                 {
-                    Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
-                    s_ImpCost[ Vec_IntSize(vImps) ] = Sml_NodeNotImpCost(pComb, *pNodesI, *pNodesK);
-                    Vec_IntPush( vImps, Imp );
+                    nImpsNonSeq++;
+                    continue;
                 }
+                if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
+                {
+                    nImpsComb++;
+                    continue;
+                }
+//                printf( "d=%d c=%d  ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) );
+
+                nImpsCollected++;
+                Imp = Sml_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) ] );
+                Vec_IntPush( vImps, Imp );
                 if ( Vec_IntSize(vImps) == nImpMaxLimit )
                     goto finish;
-            }
+            } 
         }
 finish:
-    Sml_ManStop( pComb );
-    Sml_ManStop( pSeq );
+    Fra_SmlStop( pComb );
+    Fra_SmlStop( pSeq );
+
+    // select implications with the highest cost
+    if ( Vec_IntSize(vImps) > nImpUseLimit )
+    {
+        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit );
+        Vec_IntFree( vTemp );  
+    }
 
-    // sort implications by their cost
-    pNumbers = ALLOC( int, Vec_IntSize(vImps) );
-    for ( i = 0; i < Vec_IntSize(vImps); i++ )
-        pNumbers[i] = i;
-    qsort( (void *)pNumbers, Vec_IntSize(vImps), sizeof(int), 
-            (int (*)(const void *, const void *)) Sml_CompareCost );
-    // reorder implications
-    vTemp = Vec_IntAlloc( nImpUseLimit );
-    for ( i = 0; i < nImpUseLimit; i++ )
-        Vec_IntPush( vTemp, Vec_IntEntry( vImps, pNumbers[i] ) );
-    Vec_IntFree( vImps );  vImps = vTemp;
     // dealloc
-    free( pNumbers );
-    free( s_ImpCost ); s_ImpCost = NULL;
+    free( pImpCosts ); 
     free( Vec_PtrEntry(vNodes, 0) );
     Vec_PtrFree( vNodes );
-    // order implications by the max ID involved
+    // reorder implications topologically
     qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
             (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]  ", 
+    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected, CostMin, CostMax );
+PRT( "Time", clock() - clk );
+}
     return vImps;
 }
 
@@ -678,7 +379,7 @@ finish:
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Add implication clauses to the SAT solver.]
 
   Description []
                
@@ -687,17 +388,32 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
+void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
 {
     sat_solver * pSat = p->pSat;
     Aig_Obj_t * pLeft, * pRight;
     Aig_Obj_t * pLeftF, * pRightF;
     int pLits[2], Imp, Left, Right, i, f, status;
+    int fComplL, fComplR;
     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) );
+        // check if all the nodes are present
+        for ( f = 0; f < p->pPars->nFramesK; f++ )
+        {
+            // map these info fraig
+            pLeftF = Fra_ObjFraig( pLeft, f );
+            pRightF = Fra_ObjFraig( pRight, f );
+            if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
+            {
+                Vec_IntWriteEntry( vImps, i, 0 );
+                break;
+            }
+        }
+        if ( f < p->pPars->nFramesK )
+            continue;
         // add constraints in each timeframe
         for ( f = 0; f < p->pPars->nFramesK; f++ )
         {
@@ -705,14 +421,17 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
             pLeftF = Fra_ObjFraig( pLeft, f );
             pRightF = Fra_ObjFraig( pRight, f );
             // get the corresponding SAT numbers
-            Left = Fra_ObjSatNum( Aig_Regular(pLeftF) );
-            Right = Fra_ObjSatNum( Aig_Regular(pRightF) );
+            Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
+            Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
             assert( Left > 0  && Left < p->nSatVars );
             assert( Right > 0 && Right < p->nSatVars );
+            // get the complemented attributes
+            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
+            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
             // get the constaint
-            // L => R      L' v R      L & R'
-            pLits[0] = 2 * Left  + !Aig_ObjPhaseReal(pLeftF);
-            pLits[1] = 2 * Right +  Aig_ObjPhaseReal(pRightF);
+            // L => R      L' v R     (complement = L & R')
+            pLits[0] = 2 * Left  + !fComplL;
+            pLits[1] = 2 * Right +  fComplR;
             // add contraint to solver
             if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
             {
@@ -728,6 +447,9 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
         sat_solver_delete( pSat );
         p->pSat = NULL;
     }
+//    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
+    Fra_ImpCompactArray( vImps );
+//    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
 }
 
 /**Function*************************************************************
@@ -744,9 +466,13 @@ void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
 int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
 {
     Aig_Obj_t * pLeft, * pRight;
+    Aig_Obj_t * pLeftF, * pRightF;
     int i, Imp, Left, Right, Max;
+    int fComplL, fComplR;
     Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
     {
+        if ( Imp == 0 )
+            continue;
         Left = Sml_ImpLeft(Imp);
         Right = Sml_ImpRight(Imp);
         Max = AIG_MAX( Left, Right );
@@ -754,14 +480,35 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
         if ( Max > pNode->Id )
             return i;
         // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Left );
+        pLeft  = Aig_ManObj( p->pManAig, Left );
         pRight = Aig_ManObj( p->pManAig, Right );
+        // get the corresponding FRAIG nodes
+        pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
+        pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
+        // get the complemented attributes
+        fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
+        fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
+        // 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;
+        }
         // check the implication 
         // - if true, a clause is added
         // - if false, a cex is simulated
-//        Fra_NodesAreImp( p, pLeft, pRight );
         // make sure the implication is refined
-        assert( Vec_IntEntry(vImps, Pos) == 0 );
+        if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
+        {
+            Fra_SmlResimulate( p );
+            if ( Vec_IntEntry(vImps, i) != 0 )
+                printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
+            assert( Vec_IntEntry(vImps, i) == 0 );
+        }
     }
     return i;
 }
@@ -789,10 +536,11 @@ int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
         pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
         pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
         // check if implication holds using this simulation info
-        if ( !Sml_NodeCheckImp(p->pSim, pLeft->Id, pRight->Id) )
+        if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
         {
             Vec_IntWriteEntry( vImps, i, 0 );
             RetValue = 1;
+            p->pCla->fRefinement = 1;
         }
     }
     return RetValue;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 4a7d7b7e..76cadd0f 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -198,13 +198,14 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pManAigNew;
+//    Vec_Int_t * vImps;
     int nIter, i, clk = clock(), clk2;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
@@ -223,15 +224,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
+    pPars->fUseImps   = fUseImps;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
-//    if ( fLatchCorr )
-//        Fra_ClassesLatchCorr( p );
-//    else
-        Fra_Simulate( p, 1 );
-    // refine e-classes using sequential simulation?
+//    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
+//    Fra_SmlSimulate( p, 1 );
+
+    // remember that strange bug: r iscas/blif/s5378.blif    ; st; ssw -F 4; sec -F 10
+    // refine the classes with more simulation rounds
+    p->pSml = Fra_SmlSimulateSeq( pManAig, 32, 2 );  
+    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+//    Fra_ClassesPostprocess( p->pCla );
+    // allocate new simulation manager for simulating counter-examples
+    Fra_SmlStop( p->pSml );
+    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
+
+    // select the most expressive implications
+    if ( pPars->fUseImps )
+        p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr );
  
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
@@ -251,18 +263,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         // perform AIG rewriting
         if ( p->pPars->fRewrite )
             Fra_FraigInductionRewrite( p );
-        // report the intermediate results
-        if ( fVerbose )
-        {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  N = %6d. NR = %6d.\n", 
-                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
-                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
-                Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
-        }
 
+        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-//        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        if ( pPars->fUseImps )
+            pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        else
+            pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf );
@@ -270,6 +277,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         assert( p->pSat != NULL );
         if ( p->pSat == NULL )
             printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
+        if ( pPars->fUseImps )
+        {
+            Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
+            if ( p->pSat == NULL )
+                printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
+        }
 
         // set the pointers to the manager
         Aig_ManForEachObj( p->pManFraig, pObj, i )
@@ -295,9 +308,20 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         }
         Cnf_DataFree( pCnf );
 */
+        // report the intermediate results
+        if ( fVerbose )
+        {
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  I = %6d. NR = %6d.\n", 
+                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
+                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
+                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0, Aig_ManNodeNum(p->pManFraig) );
+        }
 
         // perform sweeping
+        p->nSatCallsRecent = 0;
+        p->nSatCallsSkipped = 0;
         Fra_FraigSweep( p );
+//        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
         assert( p->vTimeouts == NULL );
         if ( p->vTimeouts )
            printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 4dcc4988..84621d60 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -77,8 +77,6 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
     pPars->fPatScores       =       0;  // enables simulation pattern scoring
     pPars->MaxScore         =      25;  // max score after which resimulation is used
     pPars->fDoSparse        =       1;  // skips sparse functions
-//    pPars->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
-//    pPars->dActConeBumpMax  =     5.0;  // the largest bump of activity
     pPars->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
     pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
     pPars->nBTLimitNode     =10000000;  // conflict limit at a node
@@ -112,15 +110,9 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->pManAig    = pManAig;
     p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
     p->nFramesAll = pPars->nFramesK + 1;
-    // allocate simulation info
-    p->nSimWords  = pPars->nSimWords * p->nFramesAll;
-    p->pSimWords  = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords );
-    // clean simulation info of the constant node
-    memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords );
     // allocate storage for sim pattern
     p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
-    p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
     p->pCla       = Fra_ClassesStart( pManAig );
@@ -238,21 +230,20 @@ void Fra_ManFinalizeComb( Fra_Man_t * p )
 void Fra_ManStop( Fra_Man_t * p )
 {
     int i;
+    if ( p->pPars->fVerbose )
+        Fra_ManPrint( p );
     for ( i = 0; i < p->nSizeAlloc; i++ )
         if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
             Vec_PtrFree( p->pMemFanins[i] );
-    if ( p->pPars->fVerbose )
-        Fra_ManPrint( p );
     if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
     if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
     if ( p->pSat )      sat_solver_delete( p->pSat );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
+    if ( p->pSml )      Fra_SmlStop( p->pSml );
     FREE( p->pMemFraig );
     FREE( p->pMemFanins );
     FREE( p->pMemSatNums );
-    FREE( p->pPatScores );
     FREE( p->pPatWords );
-    FREE( p->pSimWords );
     free( p );
 }
 
@@ -269,16 +260,16 @@ void Fra_ManStop( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_ManPrint( Fra_Man_t * p )
 {
-    double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+    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->nSimWords, p->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
+        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 );
     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 );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
-    PRT( "AIG simulation  ", p->timeSim  );
+    PRT( "AIG simulation  ", p->pSml->timeSim  );
     PRT( "AIG traversal   ", p->timeTrav );
     if ( p->timeRwr )
     {
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index a728d860..417163d5 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -66,6 +66,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
 
     p->nSatCalls++;
+    p->nSatCallsRecent++;
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
@@ -188,6 +189,110 @@ p->timeSatFail += clock() - clk;
 
 /**Function*************************************************************
 
+  Synopsis    [Runs the result of test for pObj => pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
+{
+    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
+    int status;
+
+    // make sure the nodes are not complemented
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    // if at least one of the nodes is a failed node, perform adjustments:
+    // if the backtrack limit is small, simply skip this node
+    // if the backtrack limit is > 10, take the quare root of the limit
+    nBTLimit = p->pPars->nBTLimitNode;
+/*
+    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
+    {
+        p->nSatFails++;
+        // fail immediately
+//        return -1;
+        if ( nBTLimit <= 10 )
+            return -1;
+        nBTLimit = (int)pow(nBTLimit, 0.7);
+    }
+*/
+    p->nSatCalls++;
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+    {
+        p->pSat = sat_solver_new();
+        p->nSatVars = 1;
+        sat_solver_setnvars( p->pSat, 1000 );
+    }
+
+    // if the nodes do not have SAT variables, allocate them
+    Fra_NodeAddToSolver( p, pOld, pNew );
+
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        status = sat_solver_simplify(p->pSat);
+        assert( status != 0 );
+        assert( p->pSat->qtail == p->pSat->qhead );
+    }
+
+    // prepare variable activity
+    if ( p->pPars->fConeBias )
+        Fra_SetActivityFactors( p, pOld, pNew ); 
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+clk = clock();
+//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
+//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
+    pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
+    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (sint64)nBTLimit, (sint64)0, 
+        p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        // continue solving the other implication
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        Fra_SavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatFail += clock() - clk;
+        // mark the node as the failed node
+        if ( pOld != p->pManFraig->pConst1 ) 
+            pOld->fMarkB = 1;
+        pNew->fMarkB = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Runs equivalence test for one node.]
 
   Description [Returns the fraiged node.]
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 6afa6f89..814fe59e 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -47,7 +47,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, nFrames, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +55,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index c17cea9f..a0929f99 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns random patterns to the PI node.]
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
 
   Description []
                
@@ -39,19 +39,45 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj )
+int Fra_NodeHasZeroSim( Aig_Obj_t * pObj )
 {
+    Fra_Man_t * p = pObj->pData;
     unsigned * pSims;
     int i;
-    assert( Aig_ObjIsPi(pObj) );
-    pSims = Fra_ObjSim(pObj);
-    for ( i = 0; i < p->nSimWords; i++ )
-        pSims[i] = Fra_ObjRandomSim();
+    pSims = Fra_ObjSim(p->pSml, pObj->Id);
+    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
+        if ( pSims[i] )
+            return 0;
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns constant patterns to the PI node.]
+  Synopsis    [Returns 1 if simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    Fra_Man_t * p = pObj0->pData;
+    unsigned * pSims0, * pSims1;
+    int i;
+    pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
+    pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
+    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
+        if ( pSims0[i] != pSims1[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
 
   Description []
                
@@ -60,19 +86,58 @@ void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
+unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
 {
+    Fra_Man_t * p = pObj->pData;
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
     unsigned * pSims;
+    unsigned uHash;
     int i;
-    assert( Aig_ObjIsPi(pObj) );
-    pSims = Fra_ObjSim(pObj) + p->pPars->nSimWords * iFrame;
-    for ( i = 0; i < p->pPars->nSimWords; i++ )
-        pSims[i] = fConst1? ~(unsigned)0 : 0;
+    assert( p->pSml->nWordsTotal <= 128 );
+    uHash = 0;
+    pSims = Fra_ObjSim(p->pSml, pObj->Id);
+    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
+        uHash ^= pSims[i] * s_FPrimes[i];
+    return uHash;
 }
 
+
+
+
+
 /**Function*************************************************************
 
-  Synopsis    [Assings random simulation info for the PIs.]
+  Synopsis    [Generated const 0 pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_SavePattern0( Fra_Man_t * p, int fInit )
+{
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [[Generated const 1 pattern.]
 
   Description []
                
@@ -81,31 +146,93 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFra
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AssignRandom( Fra_Man_t * p, int fInit )
+void Fra_SavePattern1( Fra_Man_t * p, int fInit )
+{
+    Aig_Obj_t * pObj;
+    int i, k, nTruePis;
+    memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
+    if ( !fInit )
+        return;
+    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    k = 0;
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_SavePattern( Fra_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
-    if ( fInit )
-    {
-        assert( Aig_ManRegNum(p->pManAig) > 0 );
-        assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
-        // assign random info for primary inputs
-        Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-            Fra_NodeAssignRandom( p, pObj );
-        // assign the initial state for the latches
-        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_NodeAssignConst( p, pObj, 0, 0 );
-    }
-    else
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Aig_ManForEachPi( p->pManFraig, pObj, i )
+        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
+            Aig_InfoSetBit( p->pPatWords, i );
+/*
+    printf( "Pattern: " );
+    Aig_ManForEachPi( p->pManFraig, pObj, i )
+        printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
+    printf( "\n" );
+*/
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the counter-example from the successful pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
+{ 
+    unsigned * pSims;
+    int i, k, BestPat, * pModel;
+    // find the word of the pattern
+    pSims = Fra_ObjSim(p->pSml, pObj->Id);
+    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
+        if ( pSims[i] )
+            break;
+    assert( i < p->pSml->nWordsTotal );
+    // find the bit of the pattern
+    for ( k = 0; k < 32; k++ )
+        if ( pSims[i] & (1 << k) )
+            break;
+    assert( k < 32 );
+    // determine the best pattern
+    BestPat = i * 32 + k;
+    // fill in the counter-example data
+    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
+    Aig_ManForEachPi( p->pManAig, pObj, i )
     {
-        Aig_ManForEachPi( p->pManAig, pObj, i )
-            Fra_NodeAssignRandom( p, pObj );
+        pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObj->Id), BestPat);
+//        printf( "%d", pModel[i] );
     }
+//    printf( "\n" );
+    // set the model
+    assert( p->pManFraig->pData == NULL );
+    p->pManFraig->pData = pModel;
+    return;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Assings distance-1 simulation info for the PIs.]
+  Synopsis    [Returns 1 if the one of the output is already non-constant 0.]
 
   Description []
                
@@ -114,48 +241,30 @@ void Fra_AssignRandom( Fra_Man_t * p, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
+int Fra_CheckOutputSims( Fra_Man_t * p )
 {
     Aig_Obj_t * pObj;
-    int f, i, k, Limit, nTruePis;
-    if ( p->pPars->nFramesK == 0 )
-    {
-        assert( p->nFramesAll == 1 );
-        // copy the PI info 
-        Aig_ManForEachPi( p->pManAig, pObj, i )
-            Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
-        // flip one bit
-        Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
-        for ( i = 0; i < Limit; i++ )
-            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
-    }
-    else
+    int i;
+    // make sure the reference simulation pattern does not detect the bug
+    pObj = Aig_ManPo( p->pManAig, 0 );
+    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
+    Aig_ManForEachPo( p->pManAig, pObj, i )
     {
-        // copy the PI info for each frame
-        nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
-        for ( f = 0; f < p->nFramesAll; f++ )
-            Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-                Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
-        // copy the latch info 
-        k = 0;
-        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 );
-        assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) );
-
-        // flip one bit of the last frame
-        if ( p->nFramesAll == 2 )
+        if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) )
         {
-            Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 );
-            for ( i = 0; i < Limit; i++ )
-                Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, i) ), i+1 );
-//            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, nTruePis*(p->nFramesAll-2) + i) ), i+1 );
+            // create the counter-example from this pattern
+            Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) );
+            return 1;
         }
     }
+    return 0;
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+  Synopsis    [Assigns random patterns to the PI node.]
 
   Description []
                
@@ -164,21 +273,19 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeHasZeroSim( Aig_Obj_t * pObj )
+void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj )
 {
-    Fra_Man_t * p = pObj->pData;
     unsigned * pSims;
     int i;
-    pSims = Fra_ObjSim(pObj);
-    for ( i = 0; i < p->nSimWords; i++ )
-        if ( pSims[i] )
-            return 0;
-    return 1;
+    assert( Aig_ObjIsPi(pObj) );
+    pSims = Fra_ObjSim( p, pObj->Id );
+    for ( i = 0; i < p->nWordsTotal; i++ )
+        pSims[i] = Fra_ObjRandomSim();
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if simulation infos are equal.]
+  Synopsis    [Assigns constant patterns to the PI node.]
 
   Description []
                
@@ -187,22 +294,19 @@ int Fra_NodeHasZeroSim( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
 {
-    Fra_Man_t * p = pObj0->pData;
-    unsigned * pSims0, * pSims1;
+    unsigned * pSims;
     int i;
-    pSims0 = Fra_ObjSim(pObj0);
-    pSims1 = Fra_ObjSim(pObj1);
-    for ( i = 0; i < p->nSimWords; i++ )
-        if ( pSims0[i] != pSims1[i] )
-            return 0;
-    return 1;
+    assert( Aig_ObjIsPi(pObj) );
+    pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
+    for ( i = 0; i < p->nWordsFrame; i++ )
+        pSims[i] = fConst1? ~(unsigned)0 : 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes hash value of the node using its simulation info.]
+  Synopsis    [Assings random simulation info for the PIs.]
 
   Description []
                
@@ -211,35 +315,80 @@ int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
+void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
 {
-    Fra_Man_t * p = pObj->pData;
-    static int s_FPrimes[128] = { 
-        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
-        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
-        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
-        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
-        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
-        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
-        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
-        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
-        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
-        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
-        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
-        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
-        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
-    };
-    unsigned * pSims;
-    unsigned uHash;
+    Aig_Obj_t * pObj;
     int i;
-    assert( p->nSimWords <= 128 );
-    uHash = 0;
-    pSims = Fra_ObjSim(pObj);
-    for ( i = 0; i < p->nSimWords; i++ )
-        uHash ^= pSims[i] * s_FPrimes[i];
-    return uHash;
+    if ( fInit )
+    {
+        assert( Aig_ManRegNum(p->pAig) > 0 );
+        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+        // assign random info for primary inputs
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Fra_SmlAssignRandom( p, pObj );
+        // assign the initial state for the latches
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_SmlAssignConst( p, pObj, 0, 0 );
+    }
+    else
+    {
+        Aig_ManForEachPi( p->pAig, pObj, i )
+            Fra_SmlAssignRandom( p, pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings distance-1 simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
+{
+    Aig_Obj_t * pObj;
+    int f, i, k, Limit, nTruePis;
+    assert( p->nFrames > 0 );
+    if ( p->nFrames == 1 )
+    {
+        // copy the PI info 
+        Aig_ManForEachPi( p->pAig, pObj, i )
+            Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+        // flip one bit
+        Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
+        for ( i = 0; i < Limit; i++ )
+            Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+    }
+    else
+    {
+        // copy the PI info for each frame
+        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
+        for ( f = 0; f < p->nFrames; f++ )
+            Aig_ManForEachPiSeq( p->pAig, pObj, i )
+                Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
+        // copy the latch info 
+        k = 0;
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
+//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
+/*
+        // flip one bit of the last frame
+        if ( p->nFrames == 2 )
+        {
+            Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
+            for ( i = 0; i < Limit; i++ )
+                Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
+//            Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
+        }
+*/
+    }
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Simulates one node.]
@@ -251,18 +400,17 @@ unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0, * pSims1;
     int fCompl, fCompl0, fCompl1, i;
-    int nSimWords = p->pPars->nSimWords;
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
-    assert( iFrame == 0 || nSimWords < p->nSimWords );
+    assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
-    pSims  = Fra_ObjSim(pObj) + nSimWords * iFrame;
-    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
-    pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
+    pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
+    pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
+    pSims1 = Fra_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
     fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
@@ -271,37 +419,37 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
     if ( fCompl0 && fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = (pSims0[i] | pSims1[i]);
         else
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = ~(pSims0[i] | pSims1[i]);
     }
     else if ( fCompl0 && !fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = (pSims0[i] | ~pSims1[i]);
         else
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = (~pSims0[i] & pSims1[i]);
     }
     else if ( !fCompl0 && fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = (~pSims0[i] | pSims1[i]);
         else
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = (pSims0[i] & ~pSims1[i]);
     }
     else // if ( !fCompl0 && !fCompl1 )
     {
         if ( fCompl )
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = ~(pSims0[i] & pSims1[i]);
         else
-            for ( i = 0; i < nSimWords; i++ )
+            for ( i = 0; i < p->nWordsFrame; i++ )
                 pSims[i] = (pSims0[i] & pSims1[i]);
     }
 }
@@ -317,26 +465,25 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0;
     int fCompl, fCompl0, i;
-    int nSimWords = p->pPars->nSimWords;
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsPo(pObj) );
-    assert( iFrame == 0 || nSimWords < p->nSimWords );
+    assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
-    pSims  = Fra_ObjSim(pObj) + nSimWords * iFrame;
-    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
+    pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
+    pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
     fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
     // copy information as it is
     if ( fCompl0 )
-        for ( i = 0; i < nSimWords; i++ )
+        for ( i = 0; i < p->nWordsFrame; i++ )
             pSims[i] = ~pSims0[i];
     else
-        for ( i = 0; i < nSimWords; i++ )
+        for ( i = 0; i < p->nWordsFrame; i++ )
             pSims[i] = pSims0[i];
 }
 
@@ -351,181 +498,26 @@ void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeTransferNext( Fra_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
+void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
 {
     unsigned * pSims0, * pSims1;
-    int i, nSimWords = p->pPars->nSimWords;
+    int i;
     assert( !Aig_IsComplement(pOut) );
     assert( !Aig_IsComplement(pIn) );
     assert( Aig_ObjIsPo(pOut) );
     assert( Aig_ObjIsPi(pIn) );
-    assert( iFrame == 0 || nSimWords < p->nSimWords );
+    assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
-    pSims0 = Fra_ObjSim(pOut) + nSimWords * iFrame;
-    pSims1 = Fra_ObjSim(pIn) + nSimWords * (iFrame+1);
+    pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
+    pSims1 = Fra_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
     // copy information as it is
-    for ( i = 0; i < nSimWords; i++ )
+    for ( i = 0; i < p->nWordsFrame; i++ )
         pSims1[i] = pSims0[i];
 }
 
 
 /**Function*************************************************************
 
-  Synopsis    [Generated const 0 pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SavePattern0( Fra_Man_t * p, int fInit )
-{
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [[Generated const 1 pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SavePattern1( Fra_Man_t * p, int fInit )
-{
-    Aig_Obj_t * pObj;
-    int i, k, nTruePis;
-    memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
-    if ( !fInit )
-        return;
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
-    k = 0;
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-        Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Copy pattern from the solver into the internal storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SavePattern( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pManFraig, pObj, i )
-        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
-            Aig_InfoSetBit( p->pPatWords, i );
-/*
-    printf( "Pattern: " );
-    Aig_ManForEachPi( p->pManFraig, pObj, i )
-        printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
-    printf( "\n" );
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans pattern scores.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_CleanPatScores( Fra_Man_t * p )
-{
-    int i, nLimit = p->nSimWords * 32;
-    for ( i = 0; i < nLimit; i++ )
-        p->pPatScores[i] = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds to pattern scores.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_AddToPatScores( Fra_Man_t * p, Aig_Obj_t * pClass, Aig_Obj_t * pClassNew )
-{
-    unsigned * pSims0, * pSims1;
-    unsigned uDiff;
-    int i, w;
-    // get hold of the simulation information
-    pSims0 = Fra_ObjSim(pClass);
-    pSims1 = Fra_ObjSim(pClassNew);
-    // iterate through the differences and record the score
-    for ( w = 0; w < p->nSimWords; w++ )
-    {
-        uDiff = pSims0[w] ^ pSims1[w];
-        if ( uDiff == 0 )
-            continue;
-        for ( i = 0; i < 32; i++ )
-            if ( uDiff & ( 1 << i ) )
-                p->pPatScores[w*32+i]++;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Selects the best pattern.]
-
-  Description [Returns 1 if such pattern is found.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SelectBestPat( Fra_Man_t * p )
-{
-    unsigned * pSims;
-    Aig_Obj_t * pObj;
-    int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
-    for ( i = 1; i < nLimit; i++ )
-    {
-        if ( MaxScore < p->pPatScores[i] )
-        {
-            MaxScore = p->pPatScores[i];
-            BestPat = i;
-        }
-    }
-    if ( MaxScore == 0 )
-        return 0;
-//    if ( MaxScore > p->pPars->MaxScore )
-//    printf( "Max score is %3d.  ", MaxScore );
-    // copy the best pattern into the selected pattern
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-    {
-        pSims = Fra_ObjSim(pObj);
-        if ( Aig_InfoHasBit(pSims, BestPat) )
-            Aig_InfoSetBit(p->pPatWords, i);
-    }
-    return MaxScore;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Simulates AIG manager.]
 
   Description [Assumes that the PI simulation info is attached.]
@@ -535,31 +527,32 @@ int Fra_SelectBestPat( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SimulateOne( Fra_Man_t * p )
+void Fra_SmlSimulateOne( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int f, i, clk;
 clk = clock();
-    for ( f = 0; f < p->nFramesAll; f++ )
+    for ( f = 0; f < p->nFrames; f++ )
     {
         // simulate the nodes
-        Aig_ManForEachNode( p->pManAig, pObj, i )
-            Fra_NodeSimulate( p, pObj, f );
-        if ( f == p->nFramesAll - 1 )
+        Aig_ManForEachNode( p->pAig, pObj, i )
+            Fra_SmlNodeSimulate( p, pObj, f );
+        if ( f == p->nFrames - 1 )
             break;
         // copy simulation info into outputs
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-            Fra_NodeCopyFanin( p, pObj, f );
+        Aig_ManForEachLiSeq( p->pAig, pObj, i )
+            Fra_SmlNodeCopyFanin( p, pObj, f );
         // copy simulation info into the inputs
-//        for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
-//            Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
-        Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, i )
-            Fra_NodeTransferNext( p, pObjLi, pObjLo, f );
+//        for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+//            Fra_SmlNodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
+        Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
+            Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
     }
 p->timeSim += clock() - clk;
 p->nSimRounds++;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Resimulates fraiging manager after finding a counter-example.]
@@ -571,43 +564,25 @@ p->nSimRounds++;
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_Resimulate( Fra_Man_t * p )
+void Fra_SmlResimulate( Fra_Man_t * p )
 {
     int nChanges, clk;
-    Fra_AssignDist1( p, p->pPatWords );
-    Fra_SimulateOne( p );
-    if ( p->pPars->fPatScores )
-        Fra_CleanPatScores( p );
+    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
+    Fra_SmlSimulateOne( p->pSml );
+//    if ( p->pPars->fPatScores )
+//        Fra_CleanPatScores( p );
     if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
     nChanges += Fra_ClassesRefine1( p->pCla );
+    if ( p->pCla->vImps )
+        nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
 p->timeRef += clock() - clk;
     if ( nChanges < 1 )
         printf( "Error: A counter-example did not refine classes!\n" );
     assert( nChanges >= 1 );
 //printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
-
-    if ( !p->pPars->fPatScores )
-        return;
-
-    // perform additional simulation using dist1 patterns derived from successful patterns
-    while ( Fra_SelectBestPat(p) > p->pPars->MaxScore )
-    {
-        Fra_AssignDist1( p, p->pPatWords );
-        Fra_SimulateOne( p );
-        Fra_CleanPatScores( p );
-        if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
-            return;
-clk = clock();
-        nChanges = Fra_ClassesRefine( p->pCla );
-        nChanges += Fra_ClassesRefine1( p->pCla );
-p->timeRef += clock() - clk;
-//printf( "Refined class!!! = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
-        if ( nChanges == 0 )
-            break;
-    }
 }
 
 /**Function*************************************************************
@@ -621,31 +596,34 @@ p->timeRef += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_Simulate( Fra_Man_t * p, int fInit )
+void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
 {
+    int fVerbose = 0;
     int nChanges, nClasses, clk;
     assert( !fInit || Aig_ManRegNum(p->pManAig) );
     // start the classes
-    Fra_AssignRandom( p, fInit );
-    Fra_SimulateOne( p );
+    Fra_SmlInitialize( p->pSml, fInit );
+    Fra_SmlSimulateOne( p->pSml );
     Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
 //    Fra_ClassesPrint( p->pCla, 0 );
-//printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
+if ( fVerbose )
+printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
 
     // refine classes by walking 0/1 patterns
     Fra_SavePattern0( p, fInit );
-    Fra_AssignDist1( p, p->pPatWords );
-    Fra_SimulateOne( p );
+    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
+    Fra_SmlSimulateOne( p->pSml );
     if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
     nChanges += Fra_ClassesRefine1( p->pCla );
 p->timeRef += clock() - clk;
-//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+if ( fVerbose )
+printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
     Fra_SavePattern1( p, fInit );
-    Fra_AssignDist1( p, p->pPatWords );
-    Fra_SimulateOne( p );
+    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
+    Fra_SmlSimulateOne( p->pSml );
     if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
         return;
 clk = clock();
@@ -653,11 +631,12 @@ clk = clock();
     nChanges += Fra_ClassesRefine1( p->pCla );
 p->timeRef += clock() - clk;
 
-//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+if ( fVerbose )
+printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
     // refine classes by random simulation
     do {
-        Fra_AssignRandom( p, fInit );
-        Fra_SimulateOne( p );
+        Fra_SmlInitialize( p->pSml, fInit );
+        Fra_SmlSimulateOne( p->pSml );
         nClasses = Vec_PtrSize(p->pCla->vClasses);
         if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
             return;
@@ -665,19 +644,20 @@ clk = clock();
         nChanges = Fra_ClassesRefine( p->pCla );
         nChanges += Fra_ClassesRefine1( p->pCla );
 p->timeRef += clock() - clk;
-//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
+if ( fVerbose )
+printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
     } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
 
 //    if ( p->pPars->fVerbose )
 //    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
 //        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-
 //    Fra_ClassesPrint( p->pCla, 0 );
 }
  
+
 /**Function*************************************************************
 
-  Synopsis    [Creates the counter-example from the successful pattern.]
+  Synopsis    [Allocates simulation manager.]
 
   Description []
                
@@ -686,40 +666,22 @@ p->timeRef += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
-{ 
-    unsigned * pSims;
-    int i, k, BestPat, * pModel;
-    // find the word of the pattern
-    pSims = Fra_ObjSim(pObj);
-    for ( i = 0; i < p->nSimWords; i++ )
-        if ( pSims[i] )
-            break;
-    assert( i < p->nSimWords );
-    // find the bit of the pattern
-    for ( k = 0; k < 32; k++ )
-        if ( pSims[i] & (1 << k) )
-            break;
-    assert( k < 32 );
-    // determine the best pattern
-    BestPat = i * 32 + k;
-    // fill in the counter-example data
-    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-    {
-        pModel[i] = Aig_InfoHasBit(Fra_ObjSim(pObj), BestPat);
-//        printf( "%d", pModel[i] );
-    }
-//    printf( "\n" );
-    // set the model
-    assert( p->pManFraig->pData == NULL );
-    p->pManFraig->pData = pModel;
-    return;
+Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, 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) * nFrames * nWordsFrame );
+    memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * nFrames * nWordsFrame );
+    p->pAig        = pAig;
+    p->nFrames     = nFrames;
+    p->nWordsFrame = nWordsFrame;
+    p->nWordsTotal = nFrames * nWordsFrame;
+    return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if the one of the output is already non-constant 0.]
+  Synopsis    [Deallocates simulation manager.]
 
   Description []
                
@@ -728,26 +690,52 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_CheckOutputSims( Fra_Man_t * p )
+void Fra_SmlStop( Fra_Sml_t * p )
 {
-    Aig_Obj_t * pObj;
-    int i;
-    // make sure the reference simulation pattern does not detect the bug
-    pObj = Aig_ManPo( p->pManAig, 0 );
-    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-    {
-        if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) )
-        {
-            // create the counter-example from this pattern
-            Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) );
-            return 1;
-        }
-    }
-    return 0;
+    free( p );
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation of the uninitialized circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
+{
+    Fra_Sml_t * p;
+    p = Fra_SmlStart( pAig, 1, nWords );
+    Fra_SmlInitialize( p, 0 );
+    Fra_SmlSimulateOne( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation of the initialized circuit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
+{
+    Fra_Sml_t * p;
+    p = Fra_SmlStart( pAig, nFrames, nWords );
+    Fra_SmlInitialize( p, 1 );
+    Fra_SmlSimulateOne( p );
+    return p;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1b5e2361..cd78f218 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10974,11 +10974,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFramesK;
     int fExdc;
-    int fImp;
+    int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10987,7 +10987,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nFramesK   = 1;
     fExdc      = 1;
-    fImp       = 0;
+    fUseImps   = 0;
     fRewrite   = 0;
     fLatchCorr = 0;
     fVerbose   = 0;
@@ -11011,7 +11011,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             fExdc ^= 1;
             break;
         case 'i':
-            fImp ^= 1;
+            fUseImps ^= 1;
             break;
         case 'r':
             fRewrite ^= 1;
@@ -11048,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11059,11 +11059,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-ilrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
-//    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "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-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4013b98d..de527306 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -892,16 +892,26 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
 {
-    Abc_Ntk_t * pNtkAig;
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pNtkAig, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+
+    // 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
+    Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
+    pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
+//    pNtkFraig = Abc_NtkDup( pNtk );
+
+    pMan = Abc_NtkToDar( pNtkFraig, 1 );
+    Abc_NtkDelete( pNtkFraig );
     if ( pMan == NULL )
         return NULL;
-//    pMan->nRegs = Abc_NtkLatchNum(pNtk);
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -960,6 +970,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
     // (note that for each functional class, fraiging leaves one representative;
     // so fraiging does not reduce the number of functions represented by nodes
     Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
     pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
     Abc_NtkDelete( pTemp );