diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-17 23:00:50 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-09-17 23:00:50 -0700 |
| commit | f14f5c92032e0a50768723af857ed9de9c792161 (patch) | |
| tree | 9997f66530030a12eaeb891b979cf96c9a4d8c0e | |
| parent | c1edeccc60099469eebe140a2b84f3fadb7110a8 (diff) | |
| download | abc-f14f5c92032e0a50768723af857ed9de9c792161.tar.gz abc-f14f5c92032e0a50768723af857ed9de9c792161.tar.bz2 abc-f14f5c92032e0a50768723af857ed9de9c792161.zip | |
Fixing obscure memory problem with 'int' on large designs.
| -rw-r--r-- | src/aig/int/intCore.c | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c index c75dd584..d6295931 100644 --- a/src/aig/int/intCore.c +++ b/src/aig/int/intCore.c @@ -159,7 +159,8 @@ clk = clock(); if ( pPars->fUseBackward ) p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); else - p->pCnfFrames = Cnf_Derive( p->pFrames, 0 ); +// p->pCnfFrames = Cnf_Derive( p->pFrames, 0 ); + p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 ); p->timeCnf += clock() - clk; // report statistics if ( pPars->fVerbose ) @@ -226,7 +227,20 @@ p->timeCnf += clock() - clk; printf( "Found a real counterexample in frame %d.\n", p->nFrames ); p->timeTotal = clock() - clkTotal; *piFrame = p->nFrames; - pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose ); +// pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose ); + { + int RetValue; + Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc; + Saig_ParBmcSetDefaultParams( pParsBmc ); + pParsBmc->nConfLimit = 100000000; + pParsBmc->nStart = p->nFrames; + pParsBmc->fVerbose = pPars->fVerbose; + RetValue = Saig_ManBmcScalable( pAig, pParsBmc ); + if ( RetValue == 1 ) + printf( "Error: The problem should be SAT but it is UNSAT.\n" ); + else if ( RetValue == -1 ) + printf( "Error: The problem timed out.\n" ); + } Inter_ManStop( p ); Inter_CheckStop( pCheck ); return 0; |