From 6a524686042a4c514f5b667d9240690d5e580a4c Mon Sep 17 00:00:00 2001
From: xiran <zhaoxiran1113@gmail.com>
Date: Sun, 12 Apr 2026 14:18:52 -0700
Subject: [PATCH] fix timing inconsistency in calculating other time in
 Ssw_ManPrintStats in sswMan.c

---
 src/proof/ssw/sswConstr.c | 3 ++-
 src/proof/ssw/sswSweep.c  | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

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;
 }