diff options
| -rw-r--r-- | src/aig/int/intCore.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c index cc6c5f5b..8fe15cda 100644 --- a/src/aig/int/intCore.c +++ b/src/aig/int/intCore.c @@ -46,7 +46,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p ) p->nFramesMax = 40; // the max number timeframes to unroll p->nFramesK = 1; // the number of timeframes to use in induction p->fRewrite = 0; // use additional rewriting to simplify timeframes - p->fTransLoop = 0; // add transition into the init state under new PI var + p->fTransLoop = 1; // add transition into the init state under new PI var p->fUsePudlak = 0; // use Pudluk interpolation procedure p->fUseOther = 0; // use other undisclosed option p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 09fd26ab..4944a43f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -13890,7 +13890,7 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) nFramesP = 0; nConfMax = 1000; nVarsMax = 1000; - fNewAlgor = 0; + fNewAlgor = 1; fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF ) @@ -13981,7 +13981,7 @@ usage: fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); fprintf( pErr, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax ); fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", nVarsMax ); - fprintf( pErr, "\t-n : toggle new algorithm [default = %s]\n", fNewAlgor? "yes": "no" ); + fprintf( pErr, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgor? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; |