131 … inline int      sat_solver3_dl(sat_solver3* s)                { return veci_size(&s->trail_lim); }  in sat_solver3_dl()
638     veci_push(&s->trail_lim,s->qtail);  in sat_solver3_decision()
651     assert( veci_size(&s->trail_lim) > 0 );  in sat_solver3_canceluntil()
652     bound   = (veci_begin(&s->trail_lim))[level];  in sat_solver3_canceluntil()
653     lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];  in sat_solver3_canceluntil()
674     veci_resize(&s->trail_lim,level);  in sat_solver3_canceluntil()
853 …start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->r…  in sat_solver3_analyze_final()
854     for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){  in sat_solver3_analyze_final()
1126     veci_new(&s->trail_lim);  in sat_solver3_new()
1191     veci_new(&s->trail_lim);  in zsat_solver3_new_seed()
1315     veci_delete(&s->trail_lim);  in sat_solver3_delete()
1360     veci_resize(&s->trail_lim, 0);  in sat_solver3_restart()
1406     veci_resize(&s->trail_lim, 0);  in zsat_solver3_restart_seed()
1465     Mem += s->trail_lim.cap * sizeof(int);  in sat_solver3_memory()
1950     veci_push(&s->trail_lim,s->qtail);  in sat_solver3_push()