diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 13:02:32 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-30 13:02:32 -0700 |
| commit | 5ace683835f29e3b4db24f9f7d0a8a4a223a164f (patch) | |
| tree | 4cea3bb7dc23e5b92dc622cf228747b9872f254a /src/base/abci | |
| parent | 851c8551c0d5314780b9430d1e7872a267e61ed2 (diff) | |
| download | abc-5ace683835f29e3b4db24f9f7d0a8a4a223a164f.tar.gz abc-5ace683835f29e3b4db24f9f7d0a8a4a223a164f.tar.bz2 abc-5ace683835f29e3b4db24f9f7d0a8a4a223a164f.zip | |
Updating bmc3 printout to show the number of failed outputs.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index adb3fe47..de686068 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -20906,6 +20906,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ); Saig_ParBmc_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc); + Vec_Ptr_t * vSeqModelVec = NULL; char * pLogFileName = NULL; int fOrDecomp = 0; int c; @@ -21056,18 +21057,19 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + vSeqModelVec = pNtk->vSeqModelVec; pNtk->vSeqModelVec = NULL; if ( pLogFileName ) Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" ); if ( pPars->fSolveAll && pPars->fDropSatOuts ) { - if ( pNtk->vSeqModelVec == NULL ) + if ( vSeqModelVec == NULL ) Abc_Print( 1,"The array of counter-examples is not available.\n" ); - else if ( Vec_PtrSize(pNtk->vSeqModelVec) != Abc_NtkPoNum(pNtk) ) + else if ( Vec_PtrSize(vSeqModelVec) != Abc_NtkPoNum(pNtk) ) Abc_Print( 1,"The array size does not match the number of outputs.\n" ); else { extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose ); - Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose ); + Abc_NtkDropSatOutputs( pNtk, vSeqModelVec, pPars->fVerbose ); pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0, -1, -1, 0, 0 ); if ( pNtkRes == NULL ) { @@ -21077,9 +21079,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); } } - if ( pNtk->vSeqModelVec ) + if ( vSeqModelVec ) { - Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); + Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); pAbc->nFrames = -1; } return 0; |