diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-30 17:24:09 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-30 17:24:09 -0800 |
| commit | 9b6ec8e84f39a773d4b1cd5d8a4b5c6aefb500d2 (patch) | |
| tree | 60243df3403fa0281acb95cb435a093257bae95b | |
| parent | cd32ae50c46d28758471fe5e8d8c99360142bfa6 (diff) | |
| download | abc-9b6ec8e84f39a773d4b1cd5d8a4b5c6aefb500d2.tar.gz abc-9b6ec8e84f39a773d4b1cd5d8a4b5c6aefb500d2.tar.bz2 abc-9b6ec8e84f39a773d4b1cd5d8a4b5c6aefb500d2.zip | |
Counter-example analysis and optimization.
| -rw-r--r-- | src/sat/bmc/bmcCexTools.c | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c index 75238bc5..f7252bc0 100644 --- a/src/sat/bmc/bmcCexTools.c +++ b/src/sat/bmc/bmcCexTools.c @@ -390,8 +390,6 @@ Abc_Cex_t * Bmc_CexEssentialBitOne( Gia_Man_t * p, Abc_Cex_t * pCexState, int iB Abc_Cex_t * pNew; Gia_Obj_t * pObj; int i, k, fCompl0, fCompl1; - int iFrame = iBit / pCexState->nPis; - int iNumber = iBit % pCexState->nPis; assert( pCexState->nRegs == 0 ); assert( iBit < pCexState->nBits ); if ( pfEqual ) @@ -405,7 +403,7 @@ Abc_Cex_t * Bmc_CexEssentialBitOne( Gia_Man_t * p, Abc_Cex_t * pCexState, int iB // simulate the remaining frames Gia_ManConst0(p)->fMark0 = 0; Gia_ManConst0(p)->fMark1 = 1; - for ( i = iFrame; i <= pCexState->iFrame; i++ ) + for ( i = iBit / pCexState->nPis; i <= pCexState->iFrame; i++ ) { Gia_ManForEachCi( p, pObj, k ) { |