Function Z3_optimize_set_initial_value 

pub unsafe extern "C" fn Z3_optimize_set_initial_value(
    c: Z3_context,
    o: Z3_optimize,
    v: Z3_ast,
    val: Z3_ast,
)

provide an initialization hint to the solver. The initialization hint is used to calibrate an initial value of the expression that represents a variable. If the variable is Boolean, the initial phase is set according to value. If the variable is an integer or real, the initial Simplex tableau is recalibrated to attempt to follow the value assignment.