summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-09-07 16:41:35 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-09-07 16:41:35 -0700
commit137a766207e27d397a8127b7e5c93c193fa108e1 (patch)
treeb9d41fdfc09d09088ac5170d99bc8dd72d72df51 /src/sat
parent23879f92000601db485d2ea226711df88c6266b9 (diff)
downloadabc-137a766207e27d397a8127b7e5c93c193fa108e1.tar.gz
abc-137a766207e27d397a8127b7e5c93c193fa108e1.tar.bz2
abc-137a766207e27d397a8127b7e5c93c193fa108e1.zip
Improvements to the new technology mapper.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcBmcAnd.c4
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 )