From 9b6ec8e84f39a773d4b1cd5d8a4b5c6aefb500d2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 30 Nov 2012 17:24:09 -0800 Subject: Counter-example analysis and optimization. --- src/sat/bmc/bmcCexTools.c | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'src/sat/bmc/bmcCexTools.c') 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 ) { -- cgit v1.2.3