diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 4 | ||||
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c9c4c587..bf871b80 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21746,7 +21746,7 @@ usage: 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 (0 = unused) [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-T num : runtime limit, in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); + Abc_Print( -2, "\t-H num : runtime limit per output, in CLOCKS_PER_SECs (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX, in seconds [default = %d]\n", pPars->nTimeOutGap ); 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 ); @@ -23588,7 +23588,7 @@ usage: Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit ); Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit ); Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); + Abc_Print( -2, "\t-H num : runtime limit per output, in CLOCKS_PER_SECs (with \"-a\") [default = %d]\n", pPars->nTimeOutOne ); Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n", pPars->nTimeOutGap ); Abc_Print( -2, "\t-a : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" ); Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 9a73b697..176a5e3e 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -81,7 +81,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio int i; p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) ); for ( i = 0; i < Saig_ManPoNum(pAig); i++ ) - p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1; + p->pTime4Outs[i] = pPars->nTimeOutOne; } if ( pPars->fSolveAll ) { diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 3a27d54c..d21a6e28 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -757,7 +757,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne ) { p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) ); for ( i = 0; i < Saig_ManPoNum(pAig); i++ ) - p->pTime4Outs[i] = nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1; + p->pTime4Outs[i] = nTimeOutOne; } return p; } @@ -1448,7 +1448,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) // stop BMC if all targets are solved if ( pPars->fSolveAll && pPars->nFailOuts + pPars->nDropOuts >= Saig_ManPoNum(pAig) ) { - Abc_Print( 1, "Stopping BMC because all targets are disproved.\n" ); + Abc_Print( 1, "Stopping BMC because all targets are disproved or timed out.\n" ); RetValue = pPars->nFailOuts ? 0 : 1; goto finish; } |