predicate adaptive_uniform(array[int] of var int: x, float: init_rate) =
  let {
    var float: rate;
  } in if status() = START then
    rate = init_rate
  elseif status() = UNSAT then
    rate = max(last_val(rate) - 0.02, 0.6)
  else
    rate = min(last_val(rate) + 0.02, 0.95)
  endif
  /\ forall(i in index_set(x)) (
    if uniform(0.0, 1.0) > rate then
      x[i] = sol(x[i])
    endif
  );