diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-17 18:36:54 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-17 18:36:54 -0700 |
| commit | 95d9aae3e7a265863114f4669e74d33338d51f81 (patch) | |
| tree | d168f00bf5757f22e269cde04ef84df553ffb5c1 /src/proof | |
| parent | 9b6efa34ad0a8a2ce33bdc5ce7e4d260562ddb14 (diff) | |
| download | abc-95d9aae3e7a265863114f4669e74d33338d51f81.tar.gz abc-95d9aae3e7a265863114f4669e74d33338d51f81.tar.bz2 abc-95d9aae3e7a265863114f4669e74d33338d51f81.zip | |
Bug fix in '&reachy' having to do with incorrect handling of resource limits.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/bbr/bbrReach.c | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index 13f4f558..0becaa39 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -249,6 +249,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D int nThreshold = 10000; clock_t clk = clock(); Vec_Ptr_t * vOnionRings; + int fixedPoint = 0; status = Cudd_ReorderingStatus( dd, &method ); if ( status ) @@ -318,8 +319,10 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext ); Cudd_RecursiveDeref( dd, bTemp ); // check if there are any new states - if ( Cudd_bddLeq( dd, bNext, bReached ) ) + if ( Cudd_bddLeq( dd, bNext, bReached ) ) { + fixedPoint = 1; break; + } // check the BDD size nBddSize = Cudd_DagSize(bNext); if ( nBddSize > pPars->nBddMax ) @@ -405,16 +408,20 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D } //ABC_PRB( dd, bReached ); Cudd_RecursiveDeref( dd, bReached ); - if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax ) - { - if ( !pPars->fSilent ) - printf( "Verified only for states reachable in %d frames. ", nIters ); - return -1; // undecided + // SPG + // + if ( fixedPoint ) { + if ( !pPars->fSilent ) { + printf( "The miter is proved unreachable after %d iterations. ", nIters ); + } + pPars->iFrame = nIters - 1; + return 1; } + assert(nIters >= pPars->nIterMax || nBddSize >= pPars->nBddMax); if ( !pPars->fSilent ) - printf( "The miter is proved unreachable after %d iterations. ", nIters ); + printf( "Verified only for states reachable in %d frames. ", nIters ); pPars->iFrame = nIters - 1; - return 1; // unreachable + return -1; // undecided } /**Function************************************************************* |