Z3 get-value in C API

Question

smtlib provides the function get-value to get specific values e.g. after optimizing a term:

(declare-const A Int)
(declare-const B Int)
(assert (> A B))
(assert (> B 10))
(assert (< A 100))
(maximize (- A B))
(check-sat)
(get-value (A B))

yields

sat
((A 99)
 (B 11))

I tried to do this with the C API however I couldn't find any equivalent operation for get-value there. Is there any similar operation? And if not how is this implemented e.g. in the Z3 shell?

EDIT: I tried the answer from christoph-wintersteiger but I only get a null result even though I would expect it to return 99 for A:

#include <stdio.h>
#include <z3.h>

int main()
{
    Z3_context context = Z3_mk_context(Z3_mk_config());
    Z3_optimize opt = Z3_mk_optimize(context);
    Z3_optimize_inc_ref(context, opt);
    Z3_ast a = Z3_mk_const(context, Z3_mk_string_symbol(context, "A"), Z3_mk_int_sort(context));
    Z3_ast b = Z3_mk_const(context, Z3_mk_string_symbol(context, "B"), Z3_mk_int_sort(context));
    Z3_ast args[] = {a, b};
    Z3_ast objective = Z3_mk_sub(context, 2, args);
    Z3_optimize_assert(context, opt, Z3_mk_gt(context, a, b));
    Z3_optimize_assert(context, opt, Z3_mk_gt(context, b, Z3_mk_unsigned_int64(context, 10, Z3_mk_int_sort(context))));
    Z3_optimize_assert(context, opt, Z3_mk_lt(context, a, Z3_mk_unsigned_int64(context, 100, Z3_mk_int_sort(context))));
    unsigned index = Z3_optimize_maximize(context, opt, objective);
    Z3_lbool result = Z3_optimize_check(context, opt, 0, 0);
    Z3_model model = Z3_optimize_get_model(context, opt);
    Z3_func_decl func_a = Z3_to_func_decl(context, a);
    Z3_ast a_result = Z3_model_get_const_interp (context, model, func_a);
    fprintf(stderr, "a: %s\n", Z3_ast_to_string(context, a_result));
    return 0;
}

// a: null

EDIT2: The link in alias' comment in combination with christoph-wintersteigers answer solved it for me.

Answer 1

In the C API values are extracted from the model objects, e.g. via Z3_solver_get_model followed by Z3_model_get_const_interp to get the value (the interpretation for a constant).