summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-04-27 16:14:40 +0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-04-27 16:14:40 +0700
commit590202e327852b35032fbbfff0389d71badffd7f (patch)
tree71572c4942801f0ffc8f860fc3ef9c963d8cd835
parentce03d5ab28d42c1ce357663590fb0f9795174079 (diff)
downloadabc-590202e327852b35032fbbfff0389d71badffd7f.tar.gz
abc-590202e327852b35032fbbfff0389d71badffd7f.tar.bz2
abc-590202e327852b35032fbbfff0389d71badffd7f.zip
Set the failed output index if ORing of outputs was done in 'int'.
-rw-r--r--src/base/abci/abc.c8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7919794f..8b9a72bf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19750,7 +19750,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Saig_ParBmc_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtkRes, * pNtk = Abc_FrameReadNtk(pAbc);
char * pLogFileName = NULL;
- int fOrDecomp = 1;
+ int fOrDecomp = 0;
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
@@ -20095,6 +20095,12 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
pAbc->Status = Abc_NtkDarBmcInter( pNtkNew, pPars, NULL );
+ if ( pAbc->Status == 0 )
+ {
+ Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ pNtkNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pMan, pNtkNew->pSeqModel );
+ Aig_ManStop( pMan );
+ }
Abc_FrameReplaceCex( pAbc, &pNtkNew->pSeqModel );
Abc_NtkDelete( pNtkNew );
}