diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:37:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:37:46 -0700 |
| commit | af4c76e21a28beac14886e68a5f7ce29e5e7303b (patch) | |
| tree | 0aad9addb18e114d1b90ccdc378371a5bb1d9f10 /src/base/abci | |
| parent | ba0d855fd4eed9439e4ce4fa6eb778cbb2250708 (diff) | |
| download | abc-af4c76e21a28beac14886e68a5f7ce29e5e7303b.tar.gz abc-af4c76e21a28beac14886e68a5f7ce29e5e7303b.tar.bz2 abc-af4c76e21a28beac14886e68a5f7ce29e5e7303b.zip | |
Disabling CNF simplification in &bmcs -g.
Diffstat (limited to 'src/base/abci')
| -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 66c0ecca..95e5f862 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40120,7 +40120,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gevwh]\n" ); + Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gvwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n", pPars->nProcs ); Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n", pPars->nConfLimit ); @@ -40128,7 +40128,7 @@ usage: Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" ); - Abc_Print( -2, "\t-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"yes": "no" ); +// Abc_Print( -2, "\t-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); |