summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-08-30 11:39:21 +0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-08-30 11:39:21 +0800
commitd103c4e28687ee9d91766c7d1057107e0100e7e3 (patch)
treecc4ce137a35dc633bc1ec5861b008a39b9afbeeb /src/sat/bmc
parentba8112ff3a64d527cf6c8a6c0d9385ca27b52c27 (diff)
downloadabc-d103c4e28687ee9d91766c7d1057107e0100e7e3.tar.gz
abc-d103c4e28687ee9d91766c7d1057107e0100e7e3.tar.bz2
abc-d103c4e28687ee9d91766c7d1057107e0100e7e3.zip
Small changes to printouts in &bmcs.
Diffstat (limited to 'src/sat/bmc')
-rw-r--r--src/sat/bmc/bmcBmcS.c6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c
index ea8ec2f6..99cc99dc 100644
--- a/src/sat/bmc/bmcBmcS.c
+++ b/src/sat/bmc/bmcBmcS.c
@@ -851,11 +851,13 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
{
+ abctime clk = Abc_Clock();
int iObj = Gia_ObjId( p->pFrames, Gia_ManCo(p->pFrames, (f+k) * Gia_ManPoNum(pGia) + i) );
int iLit = Abc_Var2Lit( Vec_IntEntry(&p->vFr2Sat, iObj), 0 );
if ( pPars->nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->nTimeOut )
break;
status = Bmcs_ManPerform_Solve( p, iLit, WorkerThread, ThData, pPars->nProcs, &Solver );
+ p->timeSat += Abc_Clock() - clk;
if ( status == l_False ) // unsat
{
if ( i == Gia_ManPoNum(pGia)-1 )
@@ -896,11 +898,11 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
ThData[i].fWorking = 1;
}
p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSat;
- Bmcs_ManPrintTime( p );
- Bmcs_ManStop( p );
if ( RetValue == -1 && !pPars->fNotVerbose )
printf( "No output failed in %d frames. ", f + (k < pPars->nFramesAdd ? k+1 : 0) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+ Bmcs_ManPrintTime( p );
+ Bmcs_ManStop( p );
return RetValue;
}