diff options
Diffstat (limited to 'src/misc')
-rw-r--r-- | src/misc/extra/extraBddMisc.c | 7 | ||||
-rw-r--r-- | src/misc/util/abc_global.h | 2 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c index 4be20a6f..66a0fc23 100644 --- a/src/misc/extra/extraBddMisc.c +++ b/src/misc/extra/extraBddMisc.c @@ -1486,19 +1486,20 @@ int Extra_bddCountCubes( DdManager * dd, DdNode ** pFuncs, int nFuncs, int fDire st__table *table = st__init_table( st__ptrcmp, st__ptrhash ); if ( table == NULL ) return -1; - dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit; for ( i = 0; i < nFuncs; i++ ) { int Count0 = 0, Count1 = 0; + dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit; if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count0, nLimit - CounterAll ) ) break; if ( fDirect ) Count1 = Count0; else { + dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + nLimit; pFuncs[i] = Cudd_Not( pFuncs[i] ); - if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, nLimit - CounterAll ) ) - break; + if ( NULL == extraBddCountCubes( dd, pFuncs[i], pFuncs[i], table, &Count1, Count0 ) ) + Count1 = Count0; pFuncs[i] = Cudd_Not( pFuncs[i] ); } CounterAll += Abc_MinInt( Count0, Count1 ); diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index ac7b2bf3..5cf351d4 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -214,7 +214,7 @@ typedef ABC_INT64_T iword; /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_INFINITY (100000000) +#define ABC_INFINITY (1000000000) #define ABC_SWAP(Type, a, b) { Type t = a; a = b; b = t; } |