我通过 C API/JNA/Scala 将 Z3 与 SMT2 一起使用，并且似乎工作得很好。
我想尝试增量求解。所以起初我使用Z3_parse_smtlib2_string翻译这个：
(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)
然后我取回Z3_ast ，通过Z3_solver_assert将其放入求解器，使用Z3_solver_check 检查并通过Z3_solver_get_model检索模型（如果检查返回令人满意，本例中就是这种情况）。到目前为止没有问题。
但是当我想另外断言这样的事情时：
(assert (= x 1))
我被困在调用Z3_parse_smtlib2_string的地方，因为它抱怨说 x 是一个未知常量。如果我还添加了declare-fun到第二个片段，我会得到一个无效的参数错误。这个变量不应该已经存在于环境中吗？我是否必须设置Z3_parse_smtlib2_string的附加参数？我怎样才能把那些从预先解析的公式中取出来？
也使用(set-option :global-decls true)不起作用，因为 Z3 告诉我初始化后无法修改此选项值。
有人知道如何解决这个问题吗？