私はjnaを使用してJavaでZ3Capiを使用しています。私はしばしば無効なメモリアクセスを取得しますが、Windows（.dll）およびmac os（.dylib）ライブラリでのみです。Linux（.so）を使用している場合は発生しません。
私は一時的にこの問題を解決しdec_ref、astと他のすべてのオブジェクトの両方に対してプロシージャを呼び出さないようにしました（私はまだinc_refprocを呼び出し、最初にを使用しますmk_context_rc）。もちろん、このソリューションは持続可能ではありません。
どこかのメモリ管理によるものだと思います。使用しただけmk_contextでもクラッシュします。
スレッドでは、JNAの単純な関数呼び出しはLinux（x64）で機能しますが、Windows（x86）では機能しません。ユーザーは同様の問題を経験し、コンパイル構成が原因であることが判明しました。
これは私が得る例外です（Mac OS X 10.6.8の場合）
Exception Type: EXC_BAD_ACCESS (SIGSEGV)
Exception Codes: KERN_INVALID_ADDRESS at 0x000000000000000c
Crashed Thread: 0 Dispatch queue: com.apple.main-thread
これが失敗の痕跡です
Thread 0 Crashed: Dispatch queue: com.apple.main-thread
0 libz3.dylib 0x00000001250d4d64 unsigned int ast_array_hash<expr>(expr* const*, unsigned int, unsigned int) + 244
1 libz3.dylib 0x00000001250cb16a ast_manager::register_node_core(ast*) + 36
2 libz3.dylib 0x00000001250cbeae ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) + 134
3 libz3.dylib 0x00000001250cc30d ast_manager::mk_app(func_decl*, unsigned int, expr* const*) + 749
4 libz3.dylib 0x000000012528c194 map_proc::reconstruct(app*) + 214
5 libz3.dylib 0x00000001254830b8 void for_each_expr_core<qe::lift_foreign_vars, obj_mark<expr, bit_vector, default_t2uint<expr> >, false, false>(qe::lift_foreign_vars&, obj_mark<expr, bit_vector, default_t2uint<expr> >&, expr*) + 760
6 libz3.dylib 0x00000001254832c9 qe::lift_foreign_vars::lift(obj_ref<expr, ast_manager>&) + 61
7 libz3.dylib 0x00000001254833a6 qe::datatype_plugin::simplify(obj_ref<expr, ast_manager>&) + 92
8 libz3.dylib 0x000000012546b1a7 qe::quant_elim_plugin::check(unsigned int, app* const*, expr*, obj_ref<expr, ast_manager>&, bool, ref_vector<app, ast_manager>&, qe::def_vector*) + 535
9 libz3.dylib 0x000000012546b8f9 qe::quant_elim_new::eliminate_block(unsigned int, app* const*, obj_ref<expr, ast_manager>&, ref_vector<app, ast_manager>&, bool, qe::def_vector*) + 445
10 libz3.dylib 0x000000012545f2cb qe::quant_elim_new::eliminate_exists(unsigned int, app* const*, obj_ref<expr, ast_manager>&, ref_vector<app, ast_manager>&, bool, qe::def_vector*) + 67
11 libz3.dylib 0x0000000125462170 qe::quant_elim_new::eliminate_exists_bind(unsigned int, app* const*, obj_ref<expr, ast_manager>&) + 88
12 libz3.dylib 0x000000012545c0ba qe::expr_quant_elim::elim(obj_ref<expr, ast_manager>&) + 1012
13 libz3.dylib 0x000000012545cb75 qe::expr_quant_elim::operator()(expr*, expr*, obj_ref<expr, ast_manager>&) + 113
14 libz3.dylib 0x000000012548b993 qe_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) + 783
15 libz3.dylib 0x00000001255debfa cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) + 14
16 libz3.dylib 0x00000001255d5e3d exec(tactic&, ref<goal> const&, sref_buffer<goal>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) + 109
17 libz3.dylib 0x0000000125070ed8 _tactic_apply + 680
18 libz3.dylib 0x00000001250711d9 Z3_tactic_apply + 105
19 jna4404318687023840668.tmp 0x000000010a00cd1c ffi_call_unix64 + 76
20 jna4404318687023840668.tmp 0x000000010a00c884 ffi_call + 644
21 jna4404318687023840668.tmp 0x000000010a003ca5 Java_com_sun_jna_Native_ffi_1prep_1cif + 1605
22 jna4404318687023840668.tmp 0x000000010a004282 Java_com_sun_jna_Native_invokePointer + 34
23 ??? 0x00000001031cfd2e 0 + 4347198766
24 ??? 0x00000001031cd658 0 + 4347188824
25 ??? 0xffb89c44ff5c4272 0 + 18426649695542329970
多分彼らは私が間違っていることを理解するのに役立つかもしれません