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

Bug fix in &bmcs.

This commit is contained in:
Alan Mishchenko 2017-08-16 14:59:36 +07:00
parent e6dd7cb5ff
commit 85eee2ea96
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/sat/bmc/bmcBmcS.c
View File

@ -575,10 +575,15 @@ void Bmcs_ManPrintFrame( Bmcs_Man_t * p, int f, int nClauses, int Solver, abctim
if ( !p->pPars->fVerbose )
return;
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
#ifdef ABC_USE_EXT_SOLVERS
Abc_Print( 1, "Var =%8.0f. ", (double)solver_varnum(p->pSats[0]) );
Abc_Print( 1, "Cla =%9.0f. ", (double)solver_clausenum(p->pSats[0]) );
Abc_Print( 1, "Learn =%9.0f. ",(double)solver_learntnum(p->pSats[0]) );
Abc_Print( 1, "Conf =%7.0f. ", (double)solver_conflictnum(p->pSats[0]) );
#else
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses );
#endif
if ( p->pPars->nProcs > 1 )
Abc_Print( 1, "S = %3d. ", Solver );
Abc_Print( 1, "%4.0f MB", 1.0*((int)Gia_ManMemory(p->pFrames) + Vec_IntMemory(&p->vFr2Sat))/(1<<20) );