diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-23 15:44:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-23 15:44:53 -0700 |
| commit | 701565eb7bd5b464f530e9816e8f4de8ceb98534 (patch) | |
| tree | 5e9d23e1b0509fcc5817e233331e50a8bc4daf16 /src/sat/bmc/bmcClp.c | |
| parent | 637da8baeaabf6f12aa8d9ec287aa675d9ea5fab (diff) | |
| download | abc-701565eb7bd5b464f530e9816e8f4de8ceb98534.tar.gz abc-701565eb7bd5b464f530e9816e8f4de8ceb98534.tar.bz2 abc-701565eb7bd5b464f530e9816e8f4de8ceb98534.zip | |
Set the default cube limit in 'satclp' to be 0.
Diffstat (limited to 'src/sat/bmc/bmcClp.c')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 4 |
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++ ) { |