luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Enabling multi-output solving in 'pdr'.

This commit is contained in:
Alan Mishchenko 2012-12-09 17:52:34 -08:00
parent ce63869fe7
commit 8355eb1d41
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/abci/abcDar.c
View File

@ -2150,7 +2150,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
Abc_Print( 1, "Some outputs (%d out of %d) are proved SAT. ",
Abc_Print( 1, "Some outputs (%d out of %d) are found to be SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
@ -2729,7 +2729,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs );
else
Abc_Print( 1, "Some outputs (%d out of %d) are proved SAT. ",
Abc_Print( 1, "Some outputs (%d out of %d) are found to be SAT. ",
nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
}
else