def hints(env: PysmtEnv) -> FrozenSet[Hint]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    delta = mgr.Symbol(delta_name, types.REAL)
    r2s = mgr.Symbol('r2s', types.INT)
    s2r = mgr.Symbol('r2s', types.INT)
    s_l = mgr.Symbol('s_l', types.BOOL)
    s_evt = mgr.Symbol('s_evt', types.BOOL)
    s_msg_id = mgr.Symbol('s_msg_id', types.INT)
    s_timeout = mgr.Symbol('s_timeout', types.REAL)
    s_c = mgr.Symbol('s_c', types.REAL)
    r_l = mgr.Symbol('r_l', types.BOOL)
    symbs = frozenset([delta, r2s, s2r, s_l, s_evt, s_msg_id, s_timeout, s_c, r_l])
    x_delta = symb_to_next(mgr, delta)
    x_r2s = symb_to_next(mgr, r2s)
    x_s2r = symb_to_next(mgr, s2r)
    x_s_l = symb_to_next(mgr, s_l)
    x_s_evt = symb_to_next(mgr, s_evt)
    x_s_msg_id = symb_to_next(mgr, s_msg_id)
    x_s_timeout = symb_to_next(mgr, s_timeout)
    x_s_c = symb_to_next(mgr, s_c)
    x_r_l = symb_to_next(mgr, r_l)
    res = []
    r0 = mgr.Real(0)
    r1 = mgr.Real(1)
    i0 = mgr.Int(0)
    i1 = mgr.Int(1)
    loc0 = Location(env, mgr.Equals(delta, r0))
    loc0.set_progress(0, mgr.Equals(x_delta, r0))
    hint = Hint('h_delta0', env, frozenset([delta]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.Equals(s2r, i0))
    loc0.set_progress(0, mgr.Equals(x_s2r, i0))
    hint = Hint('h_s2r0', env, frozenset([s2r]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, s_evt)
    loc0.set_progress(0, x_s_evt)
    hint = Hint('h_s_evt0', env, frozenset([s_evt]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.Equals(s_msg_id, i0))
    loc0.set_progress(0, mgr.Equals(x_s_msg_id, i0))
    hint = Hint('h_s_msg_id0', env, frozenset([s_msg_id]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.Equals(s_c, r0))
    loc0.set_progress(0, mgr.Equals(x_s_c, r0))
    hint = Hint('h_s_c0', env, frozenset([s_c]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, r_l)
    loc0.set_progress(0, x_r_l)
    hint = Hint('h_r_l0', env, frozenset([r_l]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s2r, i0))
    loc0.set_progress(0, mgr.Equals(x_s2r, i1))
    hint = Hint('h_s2r1', env, frozenset([s2r]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(r2s, i0))
    loc0.set_progress(0, mgr.Equals(x_r2s, i1))
    hint = Hint('h_r2s1', env, frozenset([r2s]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, s_l)
    loc0.set_progress(1, mgr.Not(x_s_l))
    loc1 = Location(env, mgr.Not(s_l))
    loc1.set_progress(0, x_s_l)
    hint = Hint('h_s_l1', env, frozenset([s_l]), symbs)
    hint.set_locs([loc0, loc1])
    res.append(hint)
    loc0 = Location(env, s_evt)
    loc0.set_progress(1, mgr.Not(x_s_evt))
    loc1 = Location(env, mgr.Not(s_evt))
    loc1.set_progress(0, x_s_evt)
    hint = Hint('h_s_evt1', env, frozenset([s_evt]), symbs)
    hint.set_locs([loc0, loc1])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s_msg_id, i0))
    loc0.set_progress(0, mgr.Equals(x_s_msg_id, mgr.Plus(s_msg_id, i1)))
    hint = Hint('h_s_msg_id1', env, frozenset([s_msg_id]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s_timeout, r0))
    loc0.set_progress(0, mgr.Equals(x_s_timeout, mgr.Plus(s_timeout, r1)))
    hint = Hint('h_s_timeout1', env, frozenset([s_timeout]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, r_l)
    loc0.set_progress(1, mgr.Not(x_r_l))
    loc1 = Location(env, mgr.Not(r_l))
    loc1.set_progress(0, x_r_l)
    hint = Hint('h_r_l1', env, frozenset([r_l]), symbs)
    hint.set_locs([loc0, loc1])
    res.append(hint)
    loc0 = Location(env, mgr.GE(delta, r0))
    loc0.set_progress(0, mgr.Equals(x_delta, mgr.Plus(delta, r1)))
    hint = Hint('h_delta2', env, frozenset([delta]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s2r, i0))
    loc0.set_progress(0, mgr.Equals(x_s2r, mgr.Plus(s2r, i1)))
    hint = Hint('h_s2r2', env, frozenset([s2r]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    return frozenset(res)
def hints(env: PysmtEnv) -> FrozenSet[Hint]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    delta = mgr.Symbol(delta_name, types.REAL)
    r2s = mgr.Symbol('r2s', types.INT)
    s2r = mgr.Symbol('r2s', types.INT)
    s_l = mgr.Symbol('s_l', types.BOOL)
    s_evt = mgr.Symbol('s_evt', types.BOOL)
    s_msg_id = mgr.Symbol('s_msg_id', types.INT)
    s_timeout = mgr.Symbol('s_timeout', types.REAL)
    s_c = mgr.Symbol('s_c', types.REAL)
    r_l = mgr.Symbol('r_l', types.BOOL)
    symbs = frozenset([delta, r2s, s2r, s_l, s_evt, s_msg_id, s_timeout, s_c, r_l])
    x_delta = symb_to_next(mgr, delta)
    x_r2s = symb_to_next(mgr, r2s)
    x_s2r = symb_to_next(mgr, s2r)
    x_s_l = symb_to_next(mgr, s_l)
    x_s_evt = symb_to_next(mgr, s_evt)
    x_s_msg_id = symb_to_next(mgr, s_msg_id)
    x_s_timeout = symb_to_next(mgr, s_timeout)
    x_s_c = symb_to_next(mgr, s_c)
    x_r_l = symb_to_next(mgr, r_l)
    res = []
    r0 = mgr.Real(0)
    r1 = mgr.Real(1)
    i0 = mgr.Int(0)
    i1 = mgr.Int(1)
    loc0 = Location(env, mgr.Equals(delta, r0))
    loc0.set_progress(0, mgr.Equals(x_delta, r0))
    hint = Hint('h_delta0', env, frozenset([delta]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.Equals(s2r, i0))
    loc0.set_progress(0, mgr.Equals(x_s2r, i0))
    hint = Hint('h_s2r0', env, frozenset([s2r]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, s_evt)
    loc0.set_progress(0, x_s_evt)
    hint = Hint('h_s_evt0', env, frozenset([s_evt]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.Equals(s_msg_id, i0))
    loc0.set_progress(0, mgr.Equals(x_s_msg_id, i0))
    hint = Hint('h_s_msg_id0', env, frozenset([s_msg_id]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.Equals(s_c, r0))
    loc0.set_progress(0, mgr.Equals(x_s_c, r0))
    hint = Hint('h_s_c0', env, frozenset([s_c]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, r_l)
    loc0.set_progress(0, x_r_l)
    hint = Hint('h_r_l0', env, frozenset([r_l]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s2r, i0))
    loc0.set_progress(0, mgr.Equals(x_s2r, i1))
    hint = Hint('h_s2r1', env, frozenset([s2r]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(r2s, i0))
    loc0.set_progress(0, mgr.Equals(x_r2s, i1))
    hint = Hint('h_r2s1', env, frozenset([r2s]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, s_l)
    loc0.set_progress(1, mgr.Not(x_s_l))
    loc1 = Location(env, mgr.Not(s_l))
    loc1.set_progress(0, x_s_l)
    hint = Hint('h_s_l1', env, frozenset([s_l]), symbs)
    hint.set_locs([loc0, loc1])
    res.append(hint)
    loc0 = Location(env, s_evt)
    loc0.set_progress(1, mgr.Not(x_s_evt))
    loc1 = Location(env, mgr.Not(s_evt))
    loc1.set_progress(0, x_s_evt)
    hint = Hint('h_s_evt1', env, frozenset([s_evt]), symbs)
    hint.set_locs([loc0, loc1])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s_msg_id, i0))
    loc0.set_progress(0, mgr.Equals(x_s_msg_id, mgr.Plus(s_msg_id, i1)))
    hint = Hint('h_s_msg_id1', env, frozenset([s_msg_id]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s_timeout, r0))
    loc0.set_progress(0, mgr.Equals(x_s_timeout, mgr.Plus(s_timeout, r1)))
    hint = Hint('h_s_timeout1', env, frozenset([s_timeout]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, r_l)
    loc0.set_progress(1, mgr.Not(x_r_l))
    loc1 = Location(env, mgr.Not(r_l))
    loc1.set_progress(0, x_r_l)
    hint = Hint('h_r_l1', env, frozenset([r_l]), symbs)
    hint.set_locs([loc0, loc1])
    res.append(hint)
    loc0 = Location(env, mgr.GE(delta, r0))
    loc0.set_progress(0, mgr.Equals(x_delta, mgr.Plus(delta, r1)))
    hint = Hint('h_delta2', env, frozenset([delta]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    loc0 = Location(env, mgr.GE(s2r, i0))
    loc0.set_progress(0, mgr.Equals(x_s2r, mgr.Plus(s2r, i1)))
    hint = Hint('h_s2r2', env, frozenset([s2r]), symbs)
    hint.set_locs([loc0])
    res.append(hint)
    return frozenset(res)