summaryrefslogtreecommitdiffstats
path: root/src/aig/int
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2011-09-17 23:00:50 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2011-09-17 23:00:50 -0700
commitf14f5c92032e0a50768723af857ed9de9c792161 (patch)
tree9997f66530030a12eaeb891b979cf96c9a4d8c0e /src/aig/int
parentc1edeccc60099469eebe140a2b84f3fadb7110a8 (diff)
downloadabc-f14f5c92032e0a50768723af857ed9de9c792161.tar.gz
abc-f14f5c92032e0a50768723af857ed9de9c792161.tar.bz2
abc-f14f5c92032e0a50768723af857ed9de9c792161.zip
Fixing obscure memory problem with 'int' on large designs.
Diffstat (limited to 'src/aig/int')
-rw-r--r--src/aig/int/intCore.c18
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;