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;
}
2 つの Z3 バージョン (Mac 64 ビットでは 4.3.1、Ubuntu 64 ビットでは 4.1) を試しました。
ヘルプ、ヒント、または回避策をいただければ幸いです。API を間違った方法で使用している可能性があります。
どうもありがとう、
エリザベス