diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 8d4c730a1..0496b2e49 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -22,6 +22,13 @@
 
 ABC_NAMESPACE_IMPL_START
 
+static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
+{
+    if ( pPars == NULL || pPars->pFunc == NULL )
+        return 0;
+    return ((int (*)(void *))pPars->pFunc)( pPars->pData );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -808,6 +815,8 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     fChanges = 1;
     for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
     {
+        if ( Cec_ParCorShouldStop( pPars ) )
+            break;
         abctime clkBmc = Abc_Clock();
         fChanges = 0;
         pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
@@ -836,6 +845,8 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
         Vec_StrFree( vStatus );
         Gia_ManStop( pSrm );
         Vec_IntFree( vOutputs );
+        if ( Cec_ParCorShouldStop( pPars ) )
+            break;
     }
     Cec_ManSimStop( pSim );
 }
@@ -975,10 +986,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     // check the base case
     if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
         Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
-    if ( pPars->pFunc )
+    if ( Cec_ParCorShouldStop( pPars ) )
     {
-        ((int (*)(void *))pPars->pFunc)( pPars->pData );
-        ((int (*)(void *))pPars->pFunc)( pPars->pData );
+        Cec_ManSimStop( pSim );
+        return 1;
     }
     if ( pPars->nStepsMax == 0 )
     {
@@ -989,6 +1000,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     // perform refinement of equivalence classes
     for ( r = 0; r < nIterMax; r++ )
     { 
+        if ( Cec_ParCorShouldStop( pPars ) )
+        {
+            Cec_ManSimStop( pSim );
+            return 1;
+        }
         if ( pPars->nStepsMax == r )
         {
             Cec_ManSimStop( pSim );
@@ -1036,8 +1052,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         Vec_StrFree( vStatus );
         Vec_IntFree( vOutputs );
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
-        if ( pPars->pFunc )
-            ((int (*)(void *))pPars->pFunc)( pPars->pData );
+        if ( Cec_ParCorShouldStop( pPars ) )
+        {
+            Cec_ManSimStop( pSim );
+            return 1;
+        }
         // quit if const is no longer there
         if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
         {
@@ -1448,4 +1467,3 @@ Gia_Man_t * Gia_ManDupStopsTest( Gia_Man_t * p )
 
 
 ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index a3a7e66f3..d8be282fa 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -512,6 +512,8 @@ clk = Abc_Clock();
     p->fRefined = 0;
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
+        if ( Ssw_ManCallbackStop(p) )
+            break;
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
@@ -540,10 +542,14 @@ clk = Abc_Clock();
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
+            if ( Ssw_ManCallbackStop(p) )
+                break;
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
             p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 );
         }
+        if ( i < Aig_ManObjNumMax(p->pAig) )
+            break;
         // quit if this is the last timeframe
         if ( f == p->pPars->nFramesK - 1 )
             break;
@@ -692,6 +698,8 @@ p->timeReduce += Abc_Clock() - clk;
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
+        if ( Ssw_ManCallbackStop(p) )
+            break;
         if ( p->pPars->fVerbose )
             Bar_ProgressUpdate( pProgress, i, NULL );
         if ( Saig_ObjIsLo(p->pAig, pObj) )
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index 1307d67c9..9add71284 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -238,6 +238,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     Aig_Man_t * pAigNew;
     int RetValue, nIter = -1, nPrev[4] = {0};
     abctime clk, clkTotal = Abc_Clock();
+    abctime nTimeToStop = p->pPars->TimeLimit > 0 ? clkTotal + (abctime)p->pPars->TimeLimit * CLOCKS_PER_SEC : 0;
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
     p->nNodesBeg = Aig_ManNodeNum(p->pAig);
@@ -251,6 +252,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     if ( !p->pPars->fLatchCorr || p->pPars->nFramesK > 1 )
     {
         p->pMSat = Ssw_SatStart( 0 );
+        if ( nTimeToStop )
+            sat_solver_set_runtime_limit( p->pMSat->pSat, nTimeToStop );
         if ( p->pPars->fConstrs )
             Ssw_ManSweepBmcConstr( p );
         else
@@ -276,11 +279,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
         Aig_ManStop( pSRed );
     }
 */
-    if ( p->pPars->pFunc )
-    {
-        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
-        ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
-    }
+    if ( Ssw_ManCallbackStop(p) || Ssw_ManCallbackStop(p) )
+        goto finalize;
     if ( p->pPars->nStepsMax == 0 )
     {
         Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
@@ -290,6 +290,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
     for ( nIter = 0; ; nIter++ )
     {
+        if ( nTimeToStop && Abc_Clock() >= nTimeToStop )
+            goto finalize;
         if ( p->pPars->nStepsMax == nIter )
         {
             Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter );
@@ -306,9 +308,13 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
             Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" );
             break;
         }
+        if ( Ssw_ManCallbackStop(p) )
+            goto finalize;
 
 clk = Abc_Clock();
         p->pMSat = Ssw_SatStart( 0 );
+        if ( nTimeToStop )
+            sat_solver_set_runtime_limit( p->pMSat->pSat, nTimeToStop );
         if ( p->pPars->fLatchCorrOpt )
         {
             RetValue = Ssw_ManSweepLatch( p );
@@ -379,8 +385,8 @@ clk = Abc_Clock();
         Ssw_ManCleanup( p );
         if ( !RetValue )
             break;
-        if ( p->pPars->pFunc )
-            ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData );
+        if ( Ssw_ManCallbackStop(p) )
+            goto finalize;
         if ( p->pPars->nLimitMax )
         {
             int nCur = Ssw_ClassesCand1Num(p->ppClasses);
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 316b2e4d1..a2654ca0b 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -407,6 +407,8 @@ p->timeReduce += Abc_Clock() - clk;
     p->iNodeStart = 0;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
+        if ( Ssw_ManCallbackStop(p) )
+            break;
         if ( p->iNodeStart == 0 )
             p->iNodeStart = i;
         if ( p->pPars->fVerbose )
diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h
index 006819237..11f60fdd9 100644
--- a/src/proof/ssw/sswInt.h
+++ b/src/proof/ssw/sswInt.h
@@ -190,6 +190,7 @@ static inline void        Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int
 
 static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t * Ssw_ObjChild1Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }
+static inline int         Ssw_ManCallbackStop( Ssw_Man_t * p ) { return (p && p->pPars && p->pPars->pFunc) ? ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ) : 0; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -299,4 +300,3 @@ ABC_NAMESPACE_HEADER_END
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index 2687e9c1c..ead977af3 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -288,6 +288,8 @@ clk = Abc_Clock();
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
+        if ( Ssw_ManCallbackStop(p) )
+            break;
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
@@ -298,12 +300,16 @@ clk = Abc_Clock();
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
+            if ( Ssw_ManCallbackStop(p) )
+                break;
             if ( p->pPars->fVerbose )
                 Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
             p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
         }
+        if ( i < Aig_ManObjNumMax(p->pAig) )
+            break;
         // quit if this is the last timeframe
         if ( f == p->pPars->nFramesK - 1 )
             break;
@@ -415,6 +421,8 @@ p->timeReduce += Abc_Clock() - clk;
     vObjPairs = (p->pPars->fEquivDump || p->pPars->fEquivDump2)? Vec_IntAlloc(1000) : NULL;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
+        if ( Ssw_ManCallbackStop(p) )
+            break;
         if ( p->pPars->fVerbose )
             Bar_ProgressUpdate( pProgress, i, NULL );
         if ( Saig_ObjIsLo(p->pAig, pObj) )