summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/proof/ssw/sswRarity.c52
-rw-r--r--src/python/pyabc.i2
2 files changed, 26 insertions, 28 deletions
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index da96d218..d2c6451e 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -549,44 +549,40 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
{
Aig_Obj_t * pObj;
- int i;
+ int i, RetValue = 0;
p->iFailPo = -1;
p->iFailPat = -1;
Saig_ManForEachPo( p->pAig, pObj, i )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
- return 0;
+ break;
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
- if ( !Ssw_RarManObjIsConst(p, pObj) )
+ if ( Ssw_RarManObjIsConst(p, pObj) )
+ continue;
+ RetValue = 1;
+ p->iFailPo = i;
+ p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
+ if ( pnSolvedNow == NULL )
+ break;
+ // remember the one solved
+ (*pnSolvedNow)++;
+ if ( p->vCexes == NULL )
+ p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
+ assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
+ Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
+ // print final report
+ if ( !fNotVerbose )
{
- p->iFailPo = i;
- p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
-
- // remember the one solved
- if ( pnSolvedNow )
- {
- (*pnSolvedNow)++;
- if ( p->vCexes == NULL )
- p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
- assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
- Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
- // print final report
- if ( !fNotVerbose )
- {
- int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
- Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
- nOutDigits, p->iFailPo, iFrame,
- nOutDigits, *pnSolvedNow,
- nOutDigits, Saig_ManPoNum(p->pAig) );
- Abc_PrintTime( 1, "Time", Time );
- }
- continue;
- }
- return 1;
+ int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
+ Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
+ nOutDigits, p->iFailPo, iFrame,
+ nOutDigits, *pnSolvedNow,
+ nOutDigits, Saig_ManPoNum(p->pAig) );
+ Abc_PrintTime( 1, "Time", Time );
}
}
- return 0;
+ return RetValue;
}
/**Function*************************************************************
diff --git a/src/python/pyabc.i b/src/python/pyabc.i
index d2fc5494..bb8cc3ca 100644
--- a/src/python/pyabc.i
+++ b/src/python/pyabc.i
@@ -238,6 +238,8 @@ Abc_Cex_t* _cex_get_vec(int i)
return NULL;
}
+ if ( pCex == (Abc_Cex_t *)1 )
+ return pCex;
return Abc_CexDup( pCex, -1 );
}