Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity).

3 files changed, 10 insertions, 6 deletions

diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index d172c4c2..40d3bc66 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -759,7 +759,6 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
     Abs_ManFreeAray( vSimInfo );
 */
-    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
     if ( fVerbose )
     {
         printf( "Running \"bmc2\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
@@ -768,6 +767,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
             nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
     } 
+    nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
+    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
     // set runtime limit
     if ( nTimeOut )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index 38c5b4ec..2124b4c3 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1076,7 +1076,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
 {
     memset( p, 0, sizeof(Saig_ParBmc_t) );
     p->nStart         =     0;    // maximum number of timeframes 
-    p->nFramesMax     =  2000;    // maximum number of timeframes 
+    p->nFramesMax     =     0;    // maximum number of timeframes 
     p->nConfLimit     =  2000;    // maximum number of conflicts at a node
     p->nConfLimitJump =     0;    // maximum number of conflicts after jumping
     p->nFramesJump    =     0;    // the number of tiemframes to jump
@@ -1120,6 +1120,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
             pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
     } 
+    pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
     // set runtime limit
     if ( p->pPars->nTimeOut )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
@@ -1246,7 +1247,9 @@ clkOther += clock() - clk2;
                         printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
                         printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
                         printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
-                        ABC_PRT( "Time", clock() - clk );
+//                        ABC_PRT( "Time", clock() - clk );
+                        printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
+                        printf( "\n" );
 //                        ABC_PRM( "Id2Var", (f+1)*p->nObjNums*4 );
 //                        ABC_PRM( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
 //                        printf( "Simples = %6d. ", p->nBufNum );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 36e3fbd0..8bf1c60e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19113,7 +19113,7 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nStart      =        0;
-    nFrames     =     2000;
+    nFrames     =        0;
     nSizeMax    =   200000;
     nBTLimit    =     2000;
     nBTLimitAll =  2000000;
@@ -19255,7 +19255,7 @@ usage:
     Abc_Print( -2, "usage: bmc2 [-SFTCGD num] [-L file] [-vh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", nStart );
-    Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", nFrames );
+    Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", nFrames );
 //    Abc_Print( -2, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeOut );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
@@ -19442,7 +19442,7 @@ usage:
     Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-sdvh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
-    Abc_Print( -2, "\t-F num : the max number of time frames [default = %d]\n", pPars->nFramesMax );
+    Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
     Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );