Variable timeframe abstraction.

src/aig/gia/giaAbsVta.c

@@ -1521,7 +1521,7 @@ finish:
             else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
                 printf( "SAT solver ran out of resources at %d conflicts in frame %d.  ", pPars->nConfLimit, f );
             else if ( p->nSeenGla >= Gia_ManCandNum(pAig) * (100-pPars->nRatioMin) / 100 )
-                printf( "Percentage of abstracted objects is less than %d in frame %d.  ", pPars->nRatioMin, f );
+                printf( "The ratio of abstracted objects is less than %d %% in frame %d.  ", pPars->nRatioMin, f );
             else
                 printf( "Abstraction stopped for unknown reason in frame %d.  ", f );
         }
@@ -1546,6 +1546,8 @@ finish:
     ABC_PRTP( "TOTAL       ", clock() - clk, clock() - clk );
 
     Vga_ManStop( p );
+
+    fflush( stdout );
     return RetValue;
 }
 

src/base/abci/abc.c

@@ -26831,7 +26831,7 @@ usage:
     Abc_Print( -2, "\t-P num : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
     Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
-    Abc_Print( -2, "\t-R num : stop when less than this %% of object is abstracted (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
+    Abc_Print( -2, "\t-R num : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
     Abc_Print( -2, "\t-t     : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");