From 0e5b950ec64466049c2a3e7510706b5c0bbe30d6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 20 May 2014 22:50:21 +0900 Subject: Adding comment to usage message in 'pdr' regarding invariant dumped when init-state is not all-0. --- src/base/abci/abc.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/base/abci/abc.c') 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" ); -- cgit v1.2.3