diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-05-20 22:50:21 +0900 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-05-20 22:50:21 +0900 |
| commit | 0e5b950ec64466049c2a3e7510706b5c0bbe30d6 (patch) | |
| tree | 129ad5b192b55766d49f829d7564c67ee8902832 | |
| parent | f30160f4be31006c768e2fca9935fb0bfb41ebf3 (diff) | |
| download | abc-0e5b950ec64466049c2a3e7510706b5c0bbe30d6.tar.gz abc-0e5b950ec64466049c2a3e7510706b5c0bbe30d6.tar.bz2 abc-0e5b950ec64466049c2a3e7510706b5c0bbe30d6.zip | |
Adding comment to usage message in 'pdr' regarding invariant dumped when init-state is not all-0.
| -rw-r--r-- | src/base/abci/abc.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fde1a59b..288623dd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -23704,7 +23704,7 @@ usage: Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" ); Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" ); Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle dumping invariant (valid if init state is all-0) [default = %s]\n", pPars->fDumpInv? "yes": "no" ); Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); |