diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index eea280293..ebb6fcce1 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -62,7 +62,8 @@ static inline double drand(double* seed) {
     *seed *= 1389796;
     q = (int)(*seed / 2147483647);
     *seed -= (double)q * 2147483647;
-    return *seed / 2147483647; }
+    return *seed * 4.6566128752457969e-10; // 1.0/2147483647.0
+}
 
 
 // Returns a random integer 0 <= x < size. Seed must never be 0.
@@ -1954,12 +1955,12 @@ int sat_solver_solve_internal(sat_solver* s)
 
     while (status == l_Undef){
         ABC_INT64_T nof_conflicts;
-        double Ratio = (s->stats.learnts == 0)? 0.0 :
-            s->stats.learnts_literals / (double)s->stats.learnts;
         if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
             break;
         if (s->verbosity >= 1)
         {
+            double Ratio = (s->stats.learnts == 0)? 0.0 :
+                s->stats.learnts_literals / (double)s->stats.learnts;
             printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
                 (double)s->stats.conflicts,
                 (double)s->stats.clauses,