summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcClp.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index d1ce061b..81f81063 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -450,7 +450,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
if ( status == l_False )
break;
// check number of cubes
- if ( Count == nCubeLim )
+ if ( nCubeLim > 0 && Count == nCubeLim )
{
//printf( "The number of cubes exceeded the limit (%d).\n", nCubeLim );
Vec_StrFreeP( &vSop );
@@ -622,7 +622,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan
}
// compute cube pairs
- for ( iCube = 0; iCube < nCubeLim; iCube++ )
+ for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
{
for ( n = 0; n < 2; n++ )
{