def hints(env: PysmtEnv) -> FrozenSet[Hint]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    pc = mgr.Symbol('pc', types.INT)
    x = mgr.Symbol('x', types.INT)
    symbs = frozenset([pc, x])
    i_5 = mgr.Int(5)
    x_x = symb_to_next(mgr, x)
    loc = Location(env, mgr.Equals(x, i_5))
    loc.set_progress(0, mgr.Equals(x_x, x))
    h_x = Hint('h_x', env, frozenset([x]), symbs)
    h_x.set_locs([loc])
    return frozenset([h_x])
def hints(env: PysmtEnv) -> FrozenSet[Hint]:
    assert isinstance(env, PysmtEnv)
    mgr = env.formula_manager
    pc = mgr.Symbol('pc', types.INT)
    x = mgr.Symbol('x', types.INT)
    symbs = frozenset([pc, x])
    i_5 = mgr.Int(5)
    x_x = symb_to_next(mgr, x)
    loc = Location(env, mgr.Equals(x, i_5))
    loc.set_progress(0, mgr.Equals(x_x, x))
    h_x = Hint('h_x', env, frozenset([x]), symbs)
    h_x.set_locs([loc])
    return frozenset([h_x])