summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcBmcAnd.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-09-10 22:16:28 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-09-10 22:16:28 -0700
commit26c0e9370ab8c2c6b54c1199da808476846bdf95 (patch)
treeb45e450d2ebc35e86077f8c73db98b11cd76f7d8 /src/sat/bmc/bmcBmcAnd.c
parent0e256dc2c234d12455df121d3cb831ba726c4cfc (diff)
downloadabc-26c0e9370ab8c2c6b54c1199da808476846bdf95.tar.gz
abc-26c0e9370ab8c2c6b54c1199da808476846bdf95.tar.bz2
abc-26c0e9370ab8c2c6b54c1199da808476846bdf95.zip
Updates for the new BMC engine.
Diffstat (limited to 'src/sat/bmc/bmcBmcAnd.c')
-rw-r--r--src/sat/bmc/bmcBmcAnd.c6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 39b4cb46..9833c692 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -717,11 +717,15 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
+ abctime clk = Abc_Clock();
p = Bmc_MnaAlloc();
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose );
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose )
- printf( "Performed unfolding for %d frames.\n", nFramesMax );
+ {
+ printf( "Performed unfolding for %d frames. ", nFramesMax );
+ Abc_PrintTime( 1, "Unfolding time", Abc_Clock() - clk );
+ }
if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL );
for ( f = 0; f < nFramesMax; f++ )