Setting infinite default conflict limits in 'bmc', 'int', 'pdr'.

src/base/abci/abc.c

@@ -18796,7 +18796,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int clk;
     // set defaults
     fVerbose   = 0;
-    nConfLimit = 100000;   
+    nConfLimit = 0;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
@@ -18931,7 +18931,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     fAndOuts   = 0;
     fNewSolver = 0;
     fVerbose   = 0;
-    nConfLimit = 100000;   
+    nConfLimit = 0;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF )
@@ -19453,8 +19453,8 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nFrames     =       20;
     nSizeMax    =   100000;
-    nBTLimit    =    10000;
-    nBTLimitAll = 10000000;
+    nBTLimit    =        0;
+    nBTLimitAll =        0;
     nNodeDelta  =     1000;
     fRewrite    =        0;
     fNewAlgo    =        1;

src/proof/int/intCore.c

@@ -45,8 +45,8 @@ ABC_NAMESPACE_IMPL_START
 void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
 { 
     memset( p, 0, sizeof(Inter_ManParams_t) );
-    p->nBTLimit     = 10000; // limit on the number of conflicts
-    p->nFramesMax   = 40;    // the max number timeframes to unroll
+    p->nBTLimit     = 0;     // limit on the number of conflicts
+    p->nFramesMax   = 0;     // the max number timeframes to unroll
     p->nSecLimit    = 0;     // time limit in seconds
     p->nFramesK     = 1;     // the number of timeframes to use in induction
     p->fRewrite     = 0;     // use additional rewriting to simplify timeframes

src/proof/pdr/pdrCore.c

@@ -47,9 +47,9 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     memset( pPars, 0, sizeof(Pdr_Par_t) );
     pPars->iOutput       =      -1;  // zero-based output number
     pPars->nRecycle      =     300;  // limit on vars for recycling
-    pPars->nFrameMax     =    5000;  // limit on number of timeframes
+    pPars->nFrameMax     =   10000;  // limit on number of timeframes
     pPars->nTimeOut      =       0;  // timeout in seconds
-    pPars->nConfLimit    =  100000;  // limit on SAT solver conflicts
+    pPars->nConfLimit    =       0;  // limit on SAT solver conflicts
     pPars->nRestLimit    =       0;  // limit on the number of proof-obligations
     pPars->fTwoRounds    =       0;  // use two rounds for generalization
     pPars->fMonoCnf      =       0;  // monolythic CNF