summaryrefslogtreecommitdiffstats
path: root/src/proof/ssc/sscSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/ssc/sscSat.c')
-rw-r--r--src/proof/ssc/sscSat.c8
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;