Integrating synthesis into the new BMC engine.

src/aig/gia/giaBalance.c

@@ -978,6 +978,7 @@ Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     Gia_Man_t * pNew, * pTemp;
     Jf_Par_t Pars, * pPars = &Pars;
     Jf_ManSetDefaultPars( pPars );
+    if ( fVerbose )     Gia_ManPrintStats( p, NULL );
     // perform balancing
     pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );

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 );