diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index d8be282fa..953ef2cfa 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -501,6 +501,7 @@ int Ssw_ManSweepBmcConstr( Ssw_Man_t * p )
     int i, f, iLits;
     abctime clk;
 clk = Abc_Clock();
+    abctime timeSatBmc = p->timeSat, timeSimSatBmc = p->timeSimSat; 
 
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -568,7 +569,7 @@ clk = Abc_Clock();
 
     // cleanup
 //    Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += Abc_Clock() - clk;
+p->timeBmc += (Abc_Clock() - clk) - (p->timeSat - timeSatBmc) - (p->timeSimSat - timeSimSatBmc);
     return p->fRefined;
 }
 
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index ead977af3..092cb1232 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -276,6 +276,7 @@ int Ssw_ManSweepBmc( Ssw_Man_t * p )
     int i, f;
     abctime clk;
 clk = Abc_Clock();
+    abctime timeSatBmc = p->timeSat, timeSimSatBmc = p->timeSimSat;
 
     // start initialized timeframes
     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
@@ -329,7 +330,7 @@ clk = Abc_Clock();
 
     // cleanup
 //    Ssw_ClassesCheck( p->ppClasses );
-p->timeBmc += Abc_Clock() - clk;
+p->timeBmc += (Abc_Clock() - clk) - (p->timeSat - timeSatBmc) - (p->timeSimSat - timeSimSatBmc);
     return p->fRefined;
 }