From 5f3ba152e5729824f78fd03e3d164de81a452d22 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Jul 2012 09:31:00 -0700 Subject: Fixed several problems when CEX is detected by &vta/&gla. --- src/aig/gia/giaAbsGla.c | 9 ++++++--- src/aig/gia/giaAbsVta.c | 1 + 2 files changed, 7 insertions(+), 3 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 1553be5f..49bcc6a0 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1925,6 +1925,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) if ( p->pPars->fVerbose ) Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); } + if ( pCex != NULL ) + break; assert( Status == 1 ); // valid core is obtained nCoreSize = Vec_IntSize( vCore ); @@ -2022,12 +2024,13 @@ finish: } else { - ABC_FREE( p->pGia->pCexSeq ); - p->pGia->pCexSeq = pCex; - if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) ) + ABC_FREE( pAig->pCexSeq ); + pAig->pCexSeq = pCex; + if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) ) Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" ); Abc_Print( 1, "Counter-example detected in frame %d. ", f ); p->pPars->iFrame = pCex->iFrame - 1; + Vec_IntFreeP( &pAig->vGateClasses ); } Abc_PrintTime( 1, "Time", clock() - clk ); if ( p->pPars->fVerbose ) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 316d5659..e2dfc90d 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1777,6 +1777,7 @@ finish: Abc_Print( 1, " Gia_VtaPerform(): CEX verification has failed!\n" ); Abc_Print( 1, "Counter-example detected in frame %d. ", f ); p->pPars->iFrame = pCex->iFrame - 1; + Vec_IntFreeP( &pAig->vObjClasses ); } Abc_PrintTime( 1, "Time", clock() - clk ); -- cgit v1.2.3