From 6014c4b11ec25aaa23dc72101c548857ab4e7367 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Oct 2013 23:17:59 -0700 Subject: Integrating synthesis into the new BMC engine. --- src/sat/bmc/bmcBmcAnd.c | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 8cdd162d..38d19a61 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -781,16 +781,14 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) printf( "Unfolding for %d frames with first non-trivial PO %d. ", nFramesMax, Gia_ManBmcFindFirst(p->pFrames) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } - if ( pPars->fVerbose ) - Gia_ManPrintStats( p->pFrames, NULL ); if ( pPars->fUseSynth ) { Gia_Man_t * pTemp = p->pFrames; p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 ); Gia_ManStop( pTemp ); - if ( pPars->fVerbose ) - Gia_ManPrintStats( p->pFrames, NULL ); } + else if ( pPars->fVerbose ) + Gia_ManPrintStats( p->pFrames, NULL ); if ( pPars->fDumpFrames ) { Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 ); -- cgit v1.2.3