diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 09:31:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 09:31:00 -0700 |
| commit | 5f3ba152e5729824f78fd03e3d164de81a452d22 (patch) | |
| tree | 5a4191397d395c4b30a7a41fe7b9239f48fe862e /src/aig | |
| parent | 8dc61f1f201f651c7e781cc7b5d34f78ebefce08 (diff) | |
| download | abc-5f3ba152e5729824f78fd03e3d164de81a452d22.tar.gz abc-5f3ba152e5729824f78fd03e3d164de81a452d22.tar.bz2 abc-5f3ba152e5729824f78fd03e3d164de81a452d22.zip | |
Fixed several problems when CEX is detected by &vta/&gla.
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 9 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 1 |
2 files changed, 7 insertions, 3 deletions
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 ); |