Bug fix in saving CEXes and CEX vectors.

This commit is contained in:
Alan Mishchenko 2013-05-21 17:28:15 -07:00
parent c31e593b09
commit b7d670ecf2
1 changed files with 9 additions and 5 deletions

View File

@ -21460,9 +21460,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
if ( vSeqModelVec )
Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
else
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
return 0;
usage:
@ -23011,8 +23013,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
// run the procedure
pAbc->Status = Abc_NtkDarPdr( pNtk, pPars );
pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
if ( pNtk->vSeqModelVec )
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
else
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
return 0;