def check_ltl(menv: msat_env, enc: LTLEncoder) -> Tuple[(Iterable, msat_term, msat_term, msat_term)]:
    assert menv
    assert isinstance(menv, msat_env)
    assert enc
    assert isinstance(enc, LTLEncoder)
    bool_type = msat_get_bool_type(menv)
    real_type = msat_get_rational_type(menv)
    i = msat_declare_function(menv, 'i', real_type)
    i = msat_make_constant(menv, i)
    r = msat_declare_function(menv, 'r', real_type)
    r = msat_make_constant(menv, r)
    l = msat_declare_function(menv, 'l', real_type)
    l = msat_make_constant(menv, l)
    inc_i = msat_declare_function(menv, 'inc_i', bool_type)
    inc_i = msat_make_constant(menv, inc_i)
    x_i = msat_declare_function(menv, name_next('i'), real_type)
    x_i = msat_make_constant(menv, x_i)
    x_r = msat_declare_function(menv, name_next('r'), real_type)
    x_r = msat_make_constant(menv, x_r)
    x_l = msat_declare_function(menv, name_next('l'), real_type)
    x_l = msat_make_constant(menv, x_l)
    x_inc_i = msat_declare_function(menv, name_next('inc_i'), bool_type)
    x_inc_i = msat_make_constant(menv, x_inc_i)
    curr2next = {i: x_i, r: x_r, l: x_l, inc_i: x_inc_i}
    zero = msat_make_number(menv, '0')
    one = msat_make_number(menv, '1')
    r_gt_0 = msat_make_gt(menv, r, zero)
    r_lt_l = msat_make_lt(menv, r, l)
    i_geq_0 = msat_make_geq(menv, i, zero)
    init = msat_make_and(menv, r_gt_0, r_lt_l)
    init = msat_make_and(menv, init, msat_make_and(menv, i_geq_0, msat_make_not(menv, inc_i)))
    init = msat_make_and(menv, init, msat_make_gt(menv, l, zero))
    trans = msat_make_equal(menv, x_r, r)
    i_lt_l = msat_make_lt(menv, i, l)
    x_i_eq_i_p_1 = msat_make_and(menv, x_inc_i, msat_make_equal(menv, x_i, msat_make_plus(menv, i, one)))
    x_i_eq_i = msat_make_and(menv, msat_make_not(menv, x_inc_i), msat_make_equal(menv, x_i, i))
    x_i_eq_i_p_1_or_i = msat_make_or(menv, x_i_eq_i_p_1, x_i_eq_i)
    x_l_eq_l = msat_make_equal(menv, x_l, l)
    x_i_eq_i_p_1_or_i_and_x_l_eq_l = msat_make_and(menv, x_i_eq_i_p_1_or_i, x_l_eq_l)
    trans = msat_make_and(menv, trans, msat_make_impl(menv, i_lt_l, x_i_eq_i_p_1_or_i_and_x_l_eq_l))
    i_geq_l = msat_make_geq(menv, i, l)
    x_i_eq_0 = msat_make_equal(menv, x_i, zero)
    x_l_eq_l_p_1 = msat_make_equal(menv, x_l, msat_make_plus(menv, l, one))
    x_i_eq_0_and_x_l_eq_l_p_1 = msat_make_and(menv, msat_make_and(menv, x_i_eq_0, x_l_eq_l_p_1), msat_make_not(menv, x_inc_i))
    trans = msat_make_and(menv, trans, msat_make_impl(menv, i_geq_l, x_i_eq_0_and_x_l_eq_l_p_1))
    G_F_x_i_gt_i = enc.make_G(enc.make_F(inc_i))
    r_gt_i = msat_make_gt(menv, r, i)
    n_G_F_r_gt_i = msat_make_not(menv, enc.make_G(enc.make_F(r_gt_i)))
    ltl = msat_make_impl(menv, G_F_x_i_gt_i, n_G_F_r_gt_i)
    return (TermMap(curr2next), init, trans, ltl)
def check_ltl(menv: msat_env, enc: LTLEncoder) -> Tuple[(Iterable, msat_term, msat_term, msat_term)]:
    assert menv
    assert isinstance(menv, msat_env)
    assert enc
    assert isinstance(enc, LTLEncoder)
    bool_type = msat_get_bool_type(menv)
    real_type = msat_get_rational_type(menv)
    i = msat_declare_function(menv, 'i', real_type)
    i = msat_make_constant(menv, i)
    r = msat_declare_function(menv, 'r', real_type)
    r = msat_make_constant(menv, r)
    l = msat_declare_function(menv, 'l', real_type)
    l = msat_make_constant(menv, l)
    inc_i = msat_declare_function(menv, 'inc_i', bool_type)
    inc_i = msat_make_constant(menv, inc_i)
    x_i = msat_declare_function(menv, name_next('i'), real_type)
    x_i = msat_make_constant(menv, x_i)
    x_r = msat_declare_function(menv, name_next('r'), real_type)
    x_r = msat_make_constant(menv, x_r)
    x_l = msat_declare_function(menv, name_next('l'), real_type)
    x_l = msat_make_constant(menv, x_l)
    x_inc_i = msat_declare_function(menv, name_next('inc_i'), bool_type)
    x_inc_i = msat_make_constant(menv, x_inc_i)
    curr2next = {i: x_i, r: x_r, l: x_l, inc_i: x_inc_i}
    zero = msat_make_number(menv, '0')
    one = msat_make_number(menv, '1')
    r_gt_0 = msat_make_gt(menv, r, zero)
    r_lt_l = msat_make_lt(menv, r, l)
    i_geq_0 = msat_make_geq(menv, i, zero)
    init = msat_make_and(menv, r_gt_0, r_lt_l)
    init = msat_make_and(menv, init, msat_make_and(menv, i_geq_0, msat_make_not(menv, inc_i)))
    init = msat_make_and(menv, init, msat_make_gt(menv, l, zero))
    trans = msat_make_equal(menv, x_r, r)
    i_lt_l = msat_make_lt(menv, i, l)
    x_i_eq_i_p_1 = msat_make_and(menv, x_inc_i, msat_make_equal(menv, x_i, msat_make_plus(menv, i, one)))
    x_i_eq_i = msat_make_and(menv, msat_make_not(menv, x_inc_i), msat_make_equal(menv, x_i, i))
    x_i_eq_i_p_1_or_i = msat_make_or(menv, x_i_eq_i_p_1, x_i_eq_i)
    x_l_eq_l = msat_make_equal(menv, x_l, l)
    x_i_eq_i_p_1_or_i_and_x_l_eq_l = msat_make_and(menv, x_i_eq_i_p_1_or_i, x_l_eq_l)
    trans = msat_make_and(menv, trans, msat_make_impl(menv, i_lt_l, x_i_eq_i_p_1_or_i_and_x_l_eq_l))
    i_geq_l = msat_make_geq(menv, i, l)
    x_i_eq_0 = msat_make_equal(menv, x_i, zero)
    x_l_eq_l_p_1 = msat_make_equal(menv, x_l, msat_make_plus(menv, l, one))
    x_i_eq_0_and_x_l_eq_l_p_1 = msat_make_and(menv, msat_make_and(menv, x_i_eq_0, x_l_eq_l_p_1), msat_make_not(menv, x_inc_i))
    trans = msat_make_and(menv, trans, msat_make_impl(menv, i_geq_l, x_i_eq_0_and_x_l_eq_l_p_1))
    G_F_x_i_gt_i = enc.make_G(enc.make_F(inc_i))
    r_gt_i = msat_make_gt(menv, r, i)
    n_G_F_r_gt_i = msat_make_not(menv, enc.make_G(enc.make_F(r_gt_i)))
    ltl = msat_make_impl(menv, G_F_x_i_gt_i, n_G_F_r_gt_i)
    return (TermMap(curr2next), init, trans, ltl)