Set the default cube limit in 'satclp' to be 0.

src/base/abci/abc.c

@@ -3102,8 +3102,8 @@ usage:
 int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes;
-    int nCubeLim = 1000;
-    int nBTLimit = 1000000;
+    int nCubeLim =        0;
+    int nBTLimit =  1000000;
     int nCostMax = 20000000;
     int fCanon   = 0;
     int fReverse = 0;

src/base/abci/abcCollapse.c

@@ -431,16 +431,19 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int n
     // order CO nodes by support size
     vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps );
     // compute cost of the largest node
-    pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 );
-    vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
-    vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) );
-    Cost = Vec_PtrSize(vDfsNodes) * Vec_IntSize(vLevel) * nCubeLim;
-    Vec_PtrFree( vDfsNodes );
-    if ( Cost > nCostMax )
+    if ( nCubeLim > 0 )
     {
-        Vec_PtrFree( vCoNodes );
-        Vec_WecFree( vSupps );
-        return NULL;
+        pNode = (Abc_Obj_t *)Vec_PtrEntry( vCoNodes, 0 );
+        vDfsNodes = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
+        vLevel = Vec_WecEntry( vSupps, Abc_ObjFaninId0(pNode) );
+        Cost = Vec_PtrSize(vDfsNodes) * Vec_IntSize(vLevel) * nCubeLim;
+        Vec_PtrFree( vDfsNodes );
+        if ( Cost > nCostMax )
+        {
+            Vec_PtrFree( vCoNodes );
+            Vec_WecFree( vSupps );
+            return NULL;
+        }
     }
     // collect CO IDs in this order
     vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );

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++ )
         {