diff options
Diffstat (limited to 'src/sat/bmc/bmcBmcAnd.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index d3998c10..8dadd619 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -314,7 +314,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) Unr_Man_t * pUnroll; Bmc_Mna_t * p = Bmc_MnaAlloc(); int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY; - int f, i, Lit, status, RetValue = -2; + int f, i=0, Lit, status, RetValue = -2; pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose ); for ( f = 0; f < nFramesMax; f++ ) { @@ -348,7 +348,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ", f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), - sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames) ); + sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); } if ( RetValue != -2 ) |