luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixed several problems when CEX is detected by &vta/&gla.

This commit is contained in:
Alan Mishchenko 2012-07-11 09:31:00 -07:00
parent 8dc61f1f20
commit 5f3ba152e5
2 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/aig/gia/giaAbsGla.c
View File

@ -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 )

1
src/aig/gia/giaAbsVta.c
View File

@ -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 );