diff options
Diffstat (limited to 'src/aig/int/intCore.c')
| -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; |