From 8b0302cdab633f6ba6b5e317e58212cb4f94c493 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 5 Jul 2012 13:32:52 -0700
Subject: Changing default conflict limits in bmc2 and bmc3 to be 0 (no limit).

---
 src/aig/saig/saigBmc3.c | 6 +++---
 src/base/abci/abc.c     | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index aeb1a34d..9107a796 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1221,7 +1221,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
     memset( p, 0, sizeof(Saig_ParBmc_t) );
     p->nStart         =     0;    // maximum number of timeframes 
     p->nFramesMax     =     0;    // maximum number of timeframes 
-    p->nConfLimit     =  2000;    // maximum number of conflicts at a node
+    p->nConfLimit     =     0;    // 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
     p->nTimeOut       =     0;    // approximate timeout in seconds
@@ -1260,8 +1260,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n", 
             Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
             Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) );
-        printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
-            pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
+        printf( "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
+            pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
     } 
     pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
     // set runtime limit
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8983ba39..3c5ccdb0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19629,13 +19629,13 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
     nStart      =        0;
     nFrames     =        0;
     nSizeMax    =   200000;
-    nBTLimit    =     2000;
-    nBTLimitAll =  2000000;
+    nBTLimit    =        0;
+    nBTLimitAll =        0;
     nNodeDelta  =     2000;
     nTimeOut    =        0;
     fRewrite    =        0;
     fNewAlgo    =        0;
-    fOrDecomp   =        1;
+    fOrDecomp   =        0;
     fVerbose    =        0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "SFNTCGDLruvh" ) ) != EOF )
-- 
cgit v1.2.3