Z3 4.0 Z3_parse_smtlib2_string

I am using Z3 with SMT2 through the C API / JNA / Scala and it seems to work very well.

I want to try a step by step solution. So first translate this using Z3_parse_smtlib2_string:

(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)

Then I go back to Z3_ast, put it in the solver through Z3_solver_assert, check it with Z3_solver_check and extract the model through Z3_solver_get_model (if the check is correct, as it was in this example). There are no problems so far.

But when I want to say something extra:

(assert (= x 1))

I am stuck at the point where Z3_parse_smtlib2_string is called because it complains that x is an unknown constant. If I add also add declare-fun to the second fragment, I get an invalid argument error. Doesn't this variable already exist in the environment? Should I set additional parameters Z3_parse_smtlib2_string? How can I get them from a strong analysis formula?

Also using (set-option: global-decls true) does not work, since Z3 tells me that this parameter value cannot be changed after initialization.

Does anyone know how to solve this problem?