summaryrefslogtreecommitdiffstats
path: root/src/proof/acec/acec2Mult.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/acec/acec2Mult.c')
-rw-r--r--src/proof/acec/acec2Mult.c4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/acec/acec2Mult.c b/src/proof/acec/acec2Mult.c
index fff6d2ac..f9cbe605 100644
--- a/src/proof/acec/acec2Mult.c
+++ b/src/proof/acec/acec2Mult.c
@@ -880,7 +880,7 @@ int Sdb_StoDiffExactlyOne2( Vec_Int_t * vAll, int * pCut )
}
Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front )
{
- int fVerbose = 1;
+ int fVerbose = 0;
Vec_Int_t * vCut, * vCounts;
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_Int_t * vResA = Vec_IntAlloc( 100 );
@@ -906,6 +906,8 @@ Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front )
Vec_IntForEachEntry( vCounts, Entry, k )
if ( Entry )
MinValue = Abc_MinInt( MinValue, Entry );
+ if ( MinValue == ABC_INFINITY )
+ return vRes;
Min = Vec_IntFind( vCounts, MinValue );
Vec_IntPush( vResA, Min );
Vec_IntWriteEntry( vCounts, Min, 0 );