From 701565eb7bd5b464f530e9816e8f4de8ceb98534 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 23 Oct 2015 15:44:53 -0700
Subject: Set the default cube limit in 'satclp' to be 0.

---
 src/sat/bmc/bmcClp.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/sat/bmc/bmcClp.c')

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++ )
         {
-- 
cgit v1.2.3