diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 168f7fc55..68601338e 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -953,7 +953,7 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
         }
         if ( status == GLUCOSE_UNDEC )
         {
-            printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
+            printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
             break;
         }
         iMint = Exa_ManEval( p );
@@ -1544,7 +1544,7 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
     if ( iMint == -1 )
         Exa3_ManPrintSolution( p, fCompl ), Res = 1;
     else if ( status == GLUCOSE_UNDEC )
-        printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
+        printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
     else 
         printf( "The problem has no solution.\n" );
     printf( "Added = %d.  Tried = %d.  ", p->nUsed[1], p->nUsed[0] );
@@ -1577,10 +1577,14 @@ void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars )
         }
         pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
         Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
-        printf( "Generated random function: %s\n", pPars->pTtStr );
+        printf( "\nIteration %d : ", i );
+        if ( pPars->nMintNum )
+            printf( "Random function has %d positive minterms.", pPars->nMintNum );
+        printf( "\n" );
+        if ( pPars->fVerbose )
+            printf( "Truth table : %s\n", pPars->pTtStr );
         nDecs += Exa3_ManExactSynthesis( pPars );
         ABC_FREE( pPars->pTtStr );
-        printf( "\n" );
     }
     printf( "Decomposable are %d (out of %d) functions (%.2f %%).\n", nDecs, pPars->nRandFuncs, 100.0*nDecs/pPars->nRandFuncs );
     ABC_FREE( pFun );