diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 16d443177..ccc890395 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -38042,11 +38042,12 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cec_ParCor_t Pars, * pPars = &Pars;
     Gia_Man_t * pTemp;
     int fPartition = 0;
+    int nFlopIncFreq = 0;
     int fUseOld = 0, c;
     Cec_ManCorSetDefaultParams( pPars );
     pPars->nProcs = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSpkrecqowvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -38116,6 +38117,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nPartSize < 0 )
                 goto usage;
             break;            
+        case 'Z':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFlopIncFreq = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFlopIncFreq < 0 )
+                goto usage;
+            break;            
         case 'p':
             fPartition ^= 1;
             break;
@@ -38168,6 +38180,31 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 0, "The network is combinational.\n" );
         return 0;
     }
+    if ( nFlopIncFreq )
+    {
+        extern Gia_Man_t * Gia_ManDupStopsAdd( Gia_Man_t * p, Vec_Int_t * vStops );
+        extern Gia_Man_t * Gia_ManDupStopsRem( Gia_Man_t * p, Vec_Int_t * vStops );
+        extern Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose );
+        Vec_Int_t * vStops = Gia_ManFindStopFlops( pAbc->pGia, nFlopIncFreq, pPars->fVerbose );
+        if ( vStops )
+        {
+            Gia_Man_t * pUsed = Gia_ManDupStopsAdd( pAbc->pGia, vStops );
+            if ( pPars->nPartSize > 0 )
+                pTemp = Gia_SignalCorrespondencePart( pUsed, pPars );
+            else if ( fUseOld )
+                pTemp = Cec_ManScorrCorrespondence( pUsed, pPars );
+            else if ( fPartition )
+                pTemp = Gia_ManScorrDivideTest( pUsed, pPars );
+            else
+                pTemp = Cec_ManLSCorrespondence( pUsed, pPars );
+            Gia_ManStop( pUsed );
+            pTemp = Gia_ManDupStopsRem( pUsed = pTemp, vStops );
+            Gia_ManStop( pUsed );
+            Abc_FrameUpdateGia( pAbc, pTemp );
+            Vec_IntFree( vStops );
+            return 0;
+        }
+    }
     if ( pPars->nPartSize > 0 )
         pTemp = Gia_SignalCorrespondencePart( pAbc->pGia, pPars );
     else if ( fUseOld )
@@ -38180,7 +38217,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &scorr [-FCGXPS num] [-pkrecqowvh]\n" );
+    Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqowvh]\n" );
     Abc_Print( -2, "\t         performs signal correpondence computation\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
@@ -38188,6 +38225,7 @@ usage:
     Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
     Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", pPars->nProcs );
     Abc_Print( -2, "\t-S num : the number of flops in one partition [default = %d]\n", pPars->nPartSize );
+    Abc_Print( -2, "\t-Z num : the average flop include frequency [default = %d]\n", nFlopIncFreq );
     Abc_Print( -2, "\t-p     : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
     Abc_Print( -2, "\t-k     : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index d1d8958fc..550ea4541 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1269,6 +1269,171 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Gia_ManCreateRegSupps( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Gia_Obj_t * pObj; int i, Id;
+    Vec_Wec_t * vSuppsR = Vec_WecStart( Gia_ManRegNum(p) );
+    Vec_Wec_t * vSupps  = Vec_WecStart( Gia_ManObjNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+        Vec_IntPush( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), i );
+    Gia_ManForEachAnd( p, pObj, Id )
+        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), 
+                          Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), 
+                          Vec_WecEntry(vSupps, Id) ); 
+    Gia_ManForEachRi( p, pObj, i )
+        Vec_IntAppend( Vec_WecEntry(vSuppsR, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
+    Vec_WecFree( vSupps );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
+    return vSuppsR;
+}
+Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose )
+{
+    Vec_Int_t * vRes = NULL, * vTemp;  int i, k, Spot, Temp, nItems = 0;
+    Vec_Wec_t * vSupps = Gia_ManCreateRegSupps( p, fVerbose );
+    Vec_Int_t * vNexts = Vec_IntStartFull( Gia_ManRegNum(p) );
+    Vec_Int_t * vAvail = Vec_IntStart( Gia_ManRegNum(p) );
+    Vec_Int_t * vHeads = Vec_IntAlloc( 10 );
+    Vec_WecForEachLevel( vSupps, vTemp, i ) {
+        if ( Vec_IntSize(vTemp) > 2 )
+            continue;
+        if ( (Spot = Vec_IntFind(vTemp, i)) >= 0 )
+            Vec_IntDrop( vTemp, Spot );
+        if ( Vec_IntSize(vTemp) != 1 )
+            continue;
+        Vec_IntWriteEntry( vNexts, i, Vec_IntEntry(vTemp, 0) );
+        Vec_IntWriteEntry( vAvail, Vec_IntEntry(vTemp, 0), 1 );
+    }
+    Vec_IntForEachEntry( vNexts, Spot, i )
+        if ( Spot >= 0 && Vec_IntEntry(vAvail, i) == 0 )
+            Vec_IntPush( vHeads, i );
+    Vec_IntForEachEntry( vHeads, Spot, i ) {
+        for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) )
+            ;
+        if ( k > 100 )
+        {
+            nItems++;
+            if ( vRes == NULL ) 
+                vRes = Vec_IntAlloc( 100 );
+            for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) )
+                if ( k % nFlopIncFreq == 0 )
+                    Vec_IntPush( vRes, Temp );
+        }
+        while ( Vec_IntEntry(vNexts, Spot) >= 0 )
+        {
+            int Next = Vec_IntEntry(vNexts, Spot);
+            Vec_IntWriteEntry( vNexts, Spot, -1 );
+            Spot = Next;
+        }
+    }
+    if ( fVerbose && vRes ) 
+        printf( "Detected %d sequence%s containing %d flops.\n", nItems, nItems > 1 ? "s":"", Vec_IntSize(vRes) );
+    Vec_IntFree( vNexts );
+    Vec_IntFree( vAvail );
+    Vec_IntFree( vHeads );
+    Vec_WecFree( vSupps );
+    return vRes;
+}
+Gia_Man_t * Gia_ManDupStopsAdd( Gia_Man_t * p, Vec_Int_t * vStops )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj; int i, Stop;
+    Vec_Int_t * vExtras = Vec_IntAlloc( Vec_IntSize(vStops) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Vec_IntForEachEntry( vStops, Stop, i )
+        Vec_IntPush( vExtras, Gia_ManAppendCi(pNew) );
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Vec_IntForEachEntry( vStops, Stop, i ) 
+    {
+        int Lit = Gia_ManCi(p, Gia_ManPiNum(p)+Stop)->Value;
+        Gia_ManCi(p, Gia_ManPiNum(p)+Stop)->Value = Vec_IntEntry(vExtras, i);
+        Vec_IntWriteEntry( vExtras, i, Lit );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Vec_IntForEachEntry( vExtras, Stop, i )
+        Gia_ManAppendCo( pNew, Stop );
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Vec_IntFree( vExtras );
+    return pNew;
+}
+void Gia_ManDupStopsRem_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+Gia_Man_t * Gia_ManDupStopsRem( Gia_Man_t * p, Vec_Int_t * vStops )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj; int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        if ( i < Gia_ManPiNum(p) - Vec_IntSize(vStops) )
+            pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachPo( p, pObj, i )
+        if ( i >= Gia_ManPoNum(p) - Vec_IntSize(vStops) )
+            Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachPi( p, pObj, i )
+        if ( i >= Gia_ManPiNum(p) - Vec_IntSize(vStops) )
+            pObj->Value = Gia_ObjFanin0Copy( Gia_ManPo(p, i - Gia_ManPiNum(p) + Gia_ManPoNum(p)) );
+    Gia_ManForEachPo( p, pObj, i )
+        if ( i < Gia_ManPoNum(p) - Vec_IntSize(vStops) )
+            Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        if ( i < Gia_ManPoNum(p) - Vec_IntSize(vStops) )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachRi( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+Gia_Man_t * Gia_ManDupStopsTest( Gia_Man_t * p )
+{
+    Vec_Int_t * vStops = Gia_ManFindStopFlops( p, 1, 1 );
+    if ( vStops == NULL )
+        return Gia_ManDup(p);
+    Gia_Man_t * pNew1 = Gia_ManDupStopsAdd( p, vStops );
+    Gia_Man_t * pNew2 = Gia_ManDupStopsRem( pNew1, vStops );
+    Gia_ManStop( pNew1 );    
+    Vec_IntFree( vStops );
+    return pNew2;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////