From 16fd67f0abdfe0ab1bba24a8d52a04ca0cac3f57 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 1 Feb 2012 14:54:32 -0800 Subject: Trying to fix a false-positive due to incorrect inductive termination check in 'int' when K is more than 1 (not fixed yet). --- src/proof/int/intCore.c | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'src/proof/int') diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c index 3bd111be..8af82f18 100644 --- a/src/proof/int/intCore.c +++ b/src/proof/int/intCore.c @@ -169,14 +169,16 @@ p->timeCnf += clock() - clk; ////////////////////////////////////////// // start containment checking - if ( !(pPars->fTransLoop || pPars->fUseBackward) ) + if ( !(pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1) ) { pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK ); // try new containment check for the initial state clk = clock(); pCnfInter2 = Cnf_Derive( p->pInter, 1 ); p->timeCnf += clock() - clk; +clk = clock(); RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut ); +p->timeEqu += clock() - clk; // assert( RetValue == 0 ); Cnf_DataFree( pCnfInter2 ); if ( p->vInters ) @@ -296,8 +298,12 @@ clk = clock(); { if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) ) { - if ( pPars->fTransLoop || pPars->fUseBackward ) - Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward ); + if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 ) + { +clk2 = clock(); + Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, Abc_MinInt(i + 1, pPars->nFramesK), pPars->fUseBackward ); +timeTemp = clock() - clk2; + } else { // new containment check clk2 = clock(); -- cgit v1.2.3