diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-23 12:41:55 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-23 12:41:55 -0800 |
| commit | c39fd3741a777034a2cbef247a1097222ac789b6 (patch) | |
| tree | 193ba416d463f0bb6dfa2e4de6a84bd0425d3e72 | |
| parent | 14457af21aeb475b6d3c42ab1926d41ef00d3887 (diff) | |
| download | abc-c39fd3741a777034a2cbef247a1097222ac789b6.tar.gz abc-c39fd3741a777034a2cbef247a1097222ac789b6.tar.bz2 abc-c39fd3741a777034a2cbef247a1097222ac789b6.zip | |
Added returning counter-example after BMC, which was recently added to 'dprove'.
| -rw-r--r-- | src/base/abci/abcDar.c | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index b032b4e4..6b8cd378 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -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; } |