def hints(env: PysmtEnv) -> FrozenSet[Hint]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    i = mgr.Symbol('i', types.REAL)
    r = mgr.Symbol('r', types.REAL)
    l = mgr.Symbol('l', types.REAL)
    inc_i = mgr.Symbol('inc_i', types.BOOL)
    symbs = frozenset([i, r, l, inc_i])
    x_i = symb_to_next(mgr, i)
    x_r = symb_to_next(mgr, r)
    x_l = symb_to_next(mgr, l)
    x_inc_i = symb_to_next(mgr, inc_i)
    res = []
    n0 = mgr.Real(0)
    n1 = mgr.Real(1)
    loc = Location(env, mgr.LE(r, n0))
    loc.set_progress(0, mgr.Equals(x_r, mgr.Minus(r, n1)))
    h_r = Hint('h_r1', env, frozenset([r]), symbs)
    h_r.set_locs([loc])
    res.append(h_r)
    loc0 = Location(env, mgr.Not(inc_i))
    loc0.set_progress(1, x_inc_i)
    loc1 = Location(env, inc_i, stutterT=x_inc_i)
    loc1.set_progress(0, mgr.Not(x_inc_i))
    h_inc = Hint('h_inc3', env, frozenset([inc_i]), symbs)
    h_inc.set_locs([loc0, loc1])
    res.append(h_inc)
    loc0 = Location(env, mgr.GE(i, n0))
    loc0.set_progress(1, mgr.Equals(x_i, mgr.Plus(i, n1)))
    loc1 = Location(env, mgr.GE(i, n0))
    loc1.set_progress(2, mgr.Equals(x_i, i))
    loc2 = Location(env, mgr.GE(i, n0))
    loc2.set_progress(0, mgr.Equals(x_i, i))
    h_i = Hint('h_i4', env, frozenset([i]), symbs)
    h_i.set_locs([loc0, loc1, loc2])
    res.append(h_i)
    loc = Location(env, mgr.GE(l, n0))
    loc.set_progress(0, mgr.Equals(x_l, mgr.Plus(l, n1)))
    h_l = Hint('h_l0', env, frozenset([l]), symbs)
    h_l.set_locs([loc])
    res.append(h_l)
    loc = Location(env, mgr.Not(inc_i))
    loc.set_progress(0, mgr.Not(x_inc_i))
    h_inc = Hint('h_inc1', env, frozenset([inc_i]), symbs)
    h_inc.set_locs([loc])
    res.append(h_inc)
    loc0 = Location(env, mgr.GE(r, n0))
    loc0.set_progress(1, mgr.Equals(x_r, r))
    loc1 = Location(env, mgr.GE(r, n0))
    loc1.set_progress(2, mgr.Equals(x_r, mgr.Plus(r, n1)))
    loc2 = Location(env, mgr.GE(r, n0))
    loc2.set_progress(0, mgr.Equals(x_r, r))
    h_r = Hint('h_r4', env, frozenset([r]), symbs)
    h_r.set_locs([loc0, loc1, loc2])
    res.append(h_r)
    loc0 = Location(env, mgr.GE(l, n0))
    loc0.set_progress(1, mgr.Equals(x_l, mgr.Plus(l, n1)))
    loc1 = Location(env, mgr.GE(l, n0))
    loc1.set_progress(0, mgr.Equals(x_l, l))
    h_l = Hint('h_l2', env, frozenset([l]), symbs)
    h_l.set_locs([loc0, loc1])
    res.append(h_l)
    loc0 = Location(env, mgr.Not(inc_i))
    loc0.set_progress(1, x_inc_i)
    loc1 = Location(env, inc_i, stutterT=x_inc_i)
    loc1.set_progress(2, mgr.Not(x_inc_i))
    loc2 = Location(env, mgr.Not(inc_i))
    loc2.set_progress(0, mgr.Not(x_inc_i))
    h_inc = Hint('h_inc4', env, frozenset([inc_i]), symbs)
    h_inc.set_locs([loc0, loc1, loc2])
    res.append(h_inc)
    loc0 = Location(env, mgr.GE(r, n0))
    loc0.set_progress(1, mgr.Equals(x_r, r))
    loc1 = Location(env, mgr.GE(r, n0))
    loc1.set_progress(0, mgr.Equals(x_r, mgr.Plus(r, n1)))
    h_r = Hint('h_r2', env, frozenset([r]), symbs)
    h_r.set_locs([loc0, loc1])
    res.append(h_r)
    loc = Location(env, mgr.GE(r, n0))
    loc.set_progress(0, mgr.Equals(x_r, mgr.Plus(r, n1)))
    h_r = Hint('h_r0', env, frozenset([r]), symbs)
    h_r.set_locs([loc])
    res.append(h_r)
    loc0 = Location(env, mgr.GE(i, n0), mgr.GE(l, n0), stutterT=mgr.Equals(x_i, mgr.Plus(i, l)))
    loc0.set_progress(1, mgr.Equals(x_i, mgr.Plus(i, n1)))
    loc1 = Location(env, mgr.GE(i, n0))
    loc1.set_progress(0, mgr.Equals(x_i, i))
    h_i = Hint('h_i3', env, frozenset([i]), symbs)
    h_i.set_locs([loc0, loc1])
    res.append(h_i)
    stutter = mgr.Equals(x_i, i)
    loc = Location(env, mgr.GE(i, n0), stutterT=stutter)
    loc.set_progress(0, mgr.Equals(x_i, mgr.Plus(i, n1)))
    h_i = Hint('h_i0', env, frozenset([i]), symbs)
    h_i.set_locs([loc])
    res.append(h_i)
    return frozenset(res)
def hints(env: PysmtEnv) -> FrozenSet[Hint]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    i = mgr.Symbol('i', types.REAL)
    r = mgr.Symbol('r', types.REAL)
    l = mgr.Symbol('l', types.REAL)
    inc_i = mgr.Symbol('inc_i', types.BOOL)
    symbs = frozenset([i, r, l, inc_i])
    x_i = symb_to_next(mgr, i)
    x_r = symb_to_next(mgr, r)
    x_l = symb_to_next(mgr, l)
    x_inc_i = symb_to_next(mgr, inc_i)
    res = []
    n0 = mgr.Real(0)
    n1 = mgr.Real(1)
    loc = Location(env, mgr.LE(r, n0))
    loc.set_progress(0, mgr.Equals(x_r, mgr.Minus(r, n1)))
    h_r = Hint('h_r1', env, frozenset([r]), symbs)
    h_r.set_locs([loc])
    res.append(h_r)
    loc0 = Location(env, mgr.Not(inc_i))
    loc0.set_progress(1, x_inc_i)
    loc1 = Location(env, inc_i, stutterT=x_inc_i)
    loc1.set_progress(0, mgr.Not(x_inc_i))
    h_inc = Hint('h_inc3', env, frozenset([inc_i]), symbs)
    h_inc.set_locs([loc0, loc1])
    res.append(h_inc)
    loc0 = Location(env, mgr.GE(i, n0))
    loc0.set_progress(1, mgr.Equals(x_i, mgr.Plus(i, n1)))
    loc1 = Location(env, mgr.GE(i, n0))
    loc1.set_progress(2, mgr.Equals(x_i, i))
    loc2 = Location(env, mgr.GE(i, n0))
    loc2.set_progress(0, mgr.Equals(x_i, i))
    h_i = Hint('h_i4', env, frozenset([i]), symbs)
    h_i.set_locs([loc0, loc1, loc2])
    res.append(h_i)
    loc = Location(env, mgr.GE(l, n0))
    loc.set_progress(0, mgr.Equals(x_l, mgr.Plus(l, n1)))
    h_l = Hint('h_l0', env, frozenset([l]), symbs)
    h_l.set_locs([loc])
    res.append(h_l)
    loc = Location(env, mgr.Not(inc_i))
    loc.set_progress(0, mgr.Not(x_inc_i))
    h_inc = Hint('h_inc1', env, frozenset([inc_i]), symbs)
    h_inc.set_locs([loc])
    res.append(h_inc)
    loc0 = Location(env, mgr.GE(r, n0))
    loc0.set_progress(1, mgr.Equals(x_r, r))
    loc1 = Location(env, mgr.GE(r, n0))
    loc1.set_progress(2, mgr.Equals(x_r, mgr.Plus(r, n1)))
    loc2 = Location(env, mgr.GE(r, n0))
    loc2.set_progress(0, mgr.Equals(x_r, r))
    h_r = Hint('h_r4', env, frozenset([r]), symbs)
    h_r.set_locs([loc0, loc1, loc2])
    res.append(h_r)
    loc0 = Location(env, mgr.GE(l, n0))
    loc0.set_progress(1, mgr.Equals(x_l, mgr.Plus(l, n1)))
    loc1 = Location(env, mgr.GE(l, n0))
    loc1.set_progress(0, mgr.Equals(x_l, l))
    h_l = Hint('h_l2', env, frozenset([l]), symbs)
    h_l.set_locs([loc0, loc1])
    res.append(h_l)
    loc0 = Location(env, mgr.Not(inc_i))
    loc0.set_progress(1, x_inc_i)
    loc1 = Location(env, inc_i, stutterT=x_inc_i)
    loc1.set_progress(2, mgr.Not(x_inc_i))
    loc2 = Location(env, mgr.Not(inc_i))
    loc2.set_progress(0, mgr.Not(x_inc_i))
    h_inc = Hint('h_inc4', env, frozenset([inc_i]), symbs)
    h_inc.set_locs([loc0, loc1, loc2])
    res.append(h_inc)
    loc0 = Location(env, mgr.GE(r, n0))
    loc0.set_progress(1, mgr.Equals(x_r, r))
    loc1 = Location(env, mgr.GE(r, n0))
    loc1.set_progress(0, mgr.Equals(x_r, mgr.Plus(r, n1)))
    h_r = Hint('h_r2', env, frozenset([r]), symbs)
    h_r.set_locs([loc0, loc1])
    res.append(h_r)
    loc = Location(env, mgr.GE(r, n0))
    loc.set_progress(0, mgr.Equals(x_r, mgr.Plus(r, n1)))
    h_r = Hint('h_r0', env, frozenset([r]), symbs)
    h_r.set_locs([loc])
    res.append(h_r)
    loc0 = Location(env, mgr.GE(i, n0), mgr.GE(l, n0), stutterT=mgr.Equals(x_i, mgr.Plus(i, l)))
    loc0.set_progress(1, mgr.Equals(x_i, mgr.Plus(i, n1)))
    loc1 = Location(env, mgr.GE(i, n0))
    loc1.set_progress(0, mgr.Equals(x_i, i))
    h_i = Hint('h_i3', env, frozenset([i]), symbs)
    h_i.set_locs([loc0, loc1])
    res.append(h_i)
    stutter = mgr.Equals(x_i, i)
    loc = Location(env, mgr.GE(i, n0), stutterT=stutter)
    loc.set_progress(0, mgr.Equals(x_i, mgr.Plus(i, n1)))
    h_i = Hint('h_i0', env, frozenset([i]), symbs)
    h_i.set_locs([loc])
    res.append(h_i)
    return frozenset(res)