diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-17 13:43:07 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-03-17 13:43:07 -0700 |
| commit | ca5d7eef2f5fbaaf5b57f32bc0b4088682ec2323 (patch) | |
| tree | 6aa5cc3cc60b4dc8a39e010bb38906bcf73128ae /src/aig/llb/llb1Reach.c | |
| parent | 464fda3fa501bca89bdf413416222ca9dacc5871 (diff) | |
| download | abc-ca5d7eef2f5fbaaf5b57f32bc0b4088682ec2323.tar.gz abc-ca5d7eef2f5fbaaf5b57f32bc0b4088682ec2323.tar.bz2 abc-ca5d7eef2f5fbaaf5b57f32bc0b4088682ec2323.zip | |
Fixing timeout in reachability engines.
Diffstat (limited to 'src/aig/llb/llb1Reach.c')
| -rw-r--r-- | src/aig/llb/llb1Reach.c | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c index 341ebd95..16b62850 100644 --- a/src/aig/llb/llb1Reach.c +++ b/src/aig/llb/llb1Reach.c @@ -629,6 +629,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo { if ( !p->pPars->fSilent ) printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = -1; return -1; } Cudd_Ref( p->ddR->bFunc ); @@ -701,6 +702,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } + p->pPars->iFrame = nIters - 1; Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL; Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; @@ -850,7 +852,10 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL; Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL; if ( bReached == NULL ) + { + p->pPars->iFrame = nIters - 1; return 0; // reachable + } // assert( bCurrent == NULL ); if ( bCurrent ) Cudd_RecursiveDeref( p->dd, bCurrent ); @@ -869,6 +874,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo { if ( !p->pPars->fSilent ) printf( "Verified only for states reachable in %d frames. ", nIters ); + p->pPars->iFrame = p->pPars->nIterMax; Cudd_RecursiveDeref( p->ddG, bReached ); return -1; // undecided } |