diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-20 20:22:10 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-20 20:22:10 -0700 |
| commit | 1d89ae52c30e81f7beac974a8b402e33c24b60c6 (patch) | |
| tree | a40761aa61d36de8cc1b35da28ccfa87cc7d025f | |
| parent | 6df122bda6a48ab61a27989b73027d617e0db626 (diff) | |
| download | abc-1d89ae52c30e81f7beac974a8b402e33c24b60c6.tar.gz abc-1d89ae52c30e81f7beac974a8b402e33c24b60c6.tar.bz2 abc-1d89ae52c30e81f7beac974a8b402e33c24b60c6.zip | |
Correcting &gla to update status as 'sat' after CEX is found.
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 5 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 5 |
2 files changed, 2 insertions, 8 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 9891a904..7654e44f 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1964,10 +1964,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) p->timeCex += clock() - clk2; if ( pCex != NULL ) - { - RetValue = 0; goto finish; - } // print the result (do not count it towards change) if ( p->pPars->fVerbose ) Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk ); @@ -2011,7 +2008,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // make sure, there was no initial abstraction (otherwise, it was invalid) assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart ); // pCex = Vga_ManDeriveCex( p ); - RetValue = 0; break; } } @@ -2084,6 +2080,7 @@ finish: Abc_Print( 1, "Counter-example detected in frame %d. ", f ); p->pPars->iFrame = pCex->iFrame - 1; Vec_IntFreeP( &pAig->vGateClasses ); + RetValue = 0; } Abc_PrintTime( 1, "Time", clock() - clk ); if ( p->pPars->fVerbose ) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 7d4bc65a..69f40af5 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1621,10 +1621,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) pCex = Vta_ManRefineAbstraction( p, f ); p->timeCex += clock() - clk2; if ( pCex != NULL ) - { - RetValue = 0; goto finish; - } // print the result (do not count it towards change) Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose ); } @@ -1653,7 +1650,6 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // make sure, there was no initial abstraction (otherwise, it was invalid) assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart ); pCex = Vga_ManDeriveCex( p ); - RetValue = 0; break; } // add the core @@ -1738,6 +1734,7 @@ finish: Abc_Print( 1, "Counter-example detected in frame %d. ", f ); p->pPars->iFrame = pCex->iFrame - 1; Vec_IntFreeP( &pAig->vObjClasses ); + RetValue = 0; } Abc_PrintTime( 1, "Time", clock() - clk ); |