# t62
# C4B:    0.50 + 1.50|[l,h]| ticks
# eocimp:

def startT62():
  var l, h, break, break1, break2

  break = 0
  break1 = 0
  break2 = 0

  assume l < h

  while break = 0:
    nondet:
      break1 = 1
    while l < h and break1 = 0:
      l = l + 1
      nondet:
        break1 = 1
      tick 1
    nondet:
      break2 = 1
    while l < h and break2 = 0:
      h = h - 1
      nondet:
        break2 = 1
      tick 1
    if l >= h:
      break = 1
    else:
      tick 1