552         s->stats.learnts++;  in sat_solver3_clause_new()
1168     s->stats.learnts          = 0;  in sat_solver3_new()
1233     s->stats.learnts          = 0;  in zsat_solver3_new_seed()
1393     s->stats.learnts          = 0;  in sat_solver3_restart()
1436     s->stats.learnts          = 0;  in zsat_solver3_restart_seed()
1499     assert( nLearnedOld == (int)s->stats.learnts );  in sat_solver3_reducedb()
1544             s->stats.learnts--;  in sat_solver3_reducedb()
1547     assert( s->stats.learnts == (unsigned)j );  in sat_solver3_reducedb()
1554     assert( Counter == (int)s->stats.learnts );  in sat_solver3_reducedb()
1592     assert( Counter == (int)s->stats.learnts );  in sat_solver3_reducedb()
1599         s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );  in sat_solver3_reducedb()
1656     s->stats.learnts = pMem->BookMarkE[1];  in sat_solver3_rollback()
1661     veci_resize(&s->act_clas,  s->stats.learnts);  in sat_solver3_rollback()
1686         s->stats.learnts          = 0;  in sat_solver3_rollback()
1912         double Ratio = (s->stats.learnts == 0)? 0.0 :  in sat_solver3_solve_internal()
1913             s->stats.learnts_literals / (double)s->stats.learnts;  in sat_solver3_solve_internal()
1923                 (double)s->stats.learnts,   in sat_solver3_solve_internal()