diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-15 11:02:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-15 11:02:53 -0700 |
| commit | d1fed2dd89bc0549655f8375832628b18b35edd9 (patch) | |
| tree | 52c34b17f9bc25f829d2cfe5d95831f52acf88d5 /src/proof/pdr | |
| parent | ab5c1692dba713599e2dbe966c0d65996943bb99 (diff) | |
| download | abc-d1fed2dd89bc0549655f8375832628b18b35edd9.tar.gz abc-d1fed2dd89bc0549655f8375832628b18b35edd9.tar.bz2 abc-d1fed2dd89bc0549655f8375832628b18b35edd9.zip | |
Fixing return value of 'pdr -a'.
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index e671d00f..16af76fd 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -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 ); |