diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 11:19:23 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 11:19:23 -0400 |
| commit | e4ab09d7711e2126d8df05002d81b3cc8a849f35 (patch) | |
| tree | fd7d92d775c1f92f7abd92d5c609d7bf81b9df97 /src/proof/ssc/sscSat.c | |
| parent | ec298486b6eb3d14398c5eb1edadc1d5ed564bf2 (diff) | |
| download | abc-e4ab09d7711e2126d8df05002d81b3cc8a849f35.tar.gz abc-e4ab09d7711e2126d8df05002d81b3cc8a849f35.tar.bz2 abc-e4ab09d7711e2126d8df05002d81b3cc8a849f35.zip | |
Sweeper return value normalization.
Diffstat (limited to 'src/proof/ssc/sscSat.c')
| -rw-r--r-- | src/proof/ssc/sscSat.c | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c index 9992f18e..ca0933ec 100644 --- a/src/proof/ssc/sscSat.c +++ b/src/proof/ssc/sscSat.c @@ -323,10 +323,12 @@ void Ssc_ManCollectSatPattern( Ssc_Man_t * p, Vec_Int_t * vPattern ) Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p ) { Vec_Int_t * vInit; - int status; - status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 ); - if ( status != l_True ) // unsat or undec + int status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 ); + if ( status == l_False ) + return (Vec_Int_t *)(ABC_PTRINT_T)1; + if ( status == l_Undef ) return NULL; + assert( status == l_True ); vInit = Vec_IntAlloc( Gia_ManCiNum(p->pFraig) ); Ssc_ManCollectSatPattern( p, vInit ); return vInit; |