diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-31 22:03:22 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-31 22:03:22 -0700 |
| commit | 679e38b012d577b9f5354465274b188f2931e8a2 (patch) | |
| tree | f325f21b30f4d90948819ed4ba324a067d23161d /src/base | |
| parent | 90867a64b4c1deb5589ac2cb50afc293c71836b9 (diff) | |
| download | abc-679e38b012d577b9f5354465274b188f2931e8a2.tar.gz abc-679e38b012d577b9f5354465274b188f2931e8a2.tar.bz2 abc-679e38b012d577b9f5354465274b188f2931e8a2.zip | |
Making per-output timeout in bmc3 -a and pdr -a work in CLOCKS_PER_SECs instead of miliseconds.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 4 |
1 files changed, 2 insertions, 2 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" ); |