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

Added returning counter-example after BMC, which was recently added to 'dprove'.

This commit is contained in:
Alan Mishchenko 2012-01-23 12:41:55 -08:00
parent 14457af21a
commit c39fd3741a
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -2270,6 +2270,10 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
printf( "SOLUTION: FAIL " );
ABC_PRT( "Time", clock() - clkTotal );
}
// return the counter-example generated
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
Aig_ManStop( pMan );
return RetValue;
}