我正在尝试通过 C API 和 smtlib2 使用 Z3 进行增量求解。不幸的是,在断言一些简单的公式、检查它、获取它的模型、断言一些额外的东西然后再次检查时,我遇到了分段违规。这也发生在没有断言新事物的情况下,即在检查、检索模型和再次检查时。这是重现错误的最小示例:
#include<z3.h>
int main()
{
Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_ast fs = Z3_parse_smtlib2_string(ctx, "(declare-fun a () Int) (assert (= a 0))", 0, 0, 0, 0, 0, 0);
Z3_solver solver = Z3_mk_solver(ctx);
Z3_solver_assert(ctx, solver, fs);
Z3_solver_check(ctx, solver);
Z3_model m = Z3_solver_get_model(ctx, solver);
Z3_solver_check(ctx, solver);
Z3_del_config(cfg);
return 0;
}
我尝试了两个 Z3 版本(Mac 64 位上的 4.3.1 和 Ubuntu 64 位上的 4.1)。
感谢任何帮助、提示或解决方法 - 也许我只是以错误的方式使用 API?
非常感谢,
伊丽莎白