luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix timing inconsistency in calculating other time in Ssw_ManPrintStats in sswMan.c

This commit is contained in:
xiran 2026-04-12 14:18:52 -07:00
parent 8aa7e12dab
commit 6a52468604
2 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/proof/ssw/sswConstr.c
View File

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

3
src/proof/ssw/sswSweep.c
View File

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