# speed_popl10_smpl_single
# C4B:    |[0,n]| ticks
# ecoimp: [n | n ≥ 0]

def start():
  var x, n

  x = 0

  while x < n:
    tick 1
    nondet:
      x = x + 1
    else:
      x = x + 1