From 4c0b78cf7f316c475d5b7c65359b9c879bad9256 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 12 Sep 2017 11:43:14 -0700 Subject: Updates to &bmcs to help debugging. --- src/base/abci/abc.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a7688741..791bad1e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40124,7 +40124,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gvwh]\n" ); + Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gevwh]\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 ); @@ -40132,7 +40132,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"); -- cgit v1.2.3