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

Fixing return value of 'pdr -a'.

This commit is contained in:
Alan Mishchenko 2013-09-15 11:02:53 -07:00
parent ab5c1692db
commit d1fed2dd89
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/proof/pdr/pdrCore.c
View File

@ -795,7 +795,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
return (Vec_PtrCountZero(p->vCexes) == Vec_PtrSize(p->vCexes)) ? 1 : 0; // UNSAT
if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
return 1; // UNSAT
if ( p->pPars->nFailOuts > 0 )
return 0; // SAT
return -1;
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );