Version abc80921_2

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

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;