我编写了一个 Z3 程序（从 test_capi.c 开始），它循环某个数字"参数"并为每个循环添加约束，这些约束依赖于前一个循环的约束。这个想法是每个周期选择 2 个项目 a，d，这些项目要么是相同的旧 a，d 要么是pointer_a选择的新 a，d，pointer_d从有序列表中选择u_a，u_d。
该代码适用于某些循环计数，而不适用于其他循环计数（给出 sat 与分段错误）。更奇怪的是，代码工作的循环计数的编号在更改代码时会发生变化。所以下面的代码有效并且是 SAT（我已经选择了 n_ABCD=check3 ），但它只给出了从 2 到 10 的"参数"的结果，除了 6，参数=8、16、32 可能是其他一些数字，但我至少尝试了这些;它不适用于 31、33、64、128 和 512。当我将循环分成 2 个循环时，一个用于 pointer_a[] 和 pointer_d[] 约束，另一个用于check_v操作，代码适用于最多 9 的"参数"，然后适用于 12、14、17 和 27，我没有其他更大的数字。目标是将其运行到参数=1024 甚至更多。
为什么代码只能针对某些数字运行而不为其他数字运行的任何解释？它是否与选择正在评估的任意术语的工作方式有关？（make_var_feasible，update_and_pivot...如下面的 GDB 跟踪更多）
char cated_string[20];
for(int i = 0; i< parameter; i++){
sprintf(cated_string,"%s%d%s", "pointer_d[", i, "]");
pointer_d[i] = mk_var(ctx, cated_string , bv32_sort);
sprintf(cated_string,"%s%d%s", "pointer_a[", i, "]");
pointer_a[i] = mk_var(ctx, cated_string , bv32_sort);
}
u_d_ast = mk_var(ctx, "u_d_ast", array_sort);
u_a_ast = mk_var(ctx, "u_a_ast", array_sort);
for (unsigned int i = 0; i < parameter; i++) {index = Z3_mk_unsigned_int(ctx, i, bv32_sort);
u_d_ast = Z3_mk_store(ctx, u_d_ast, index, u_d[i]);
u_a_ast = Z3_mk_store(ctx, u_a_ast, index, u_a[i]);
}
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, pointer_d[0], n_zero) );
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, pointer_a[0], n_zero) );
a_v = mk_var(ctx, "a_v", array_sort);
d_v = mk_var(ctx, "d_v", array_sort);
check_v = mk_var(ctx, "check_v" , array_sort);
check_v = Z3_mk_store(ctx, check_v, n_zero, n_zero );
a_v = Z3_mk_store(ctx, a_v, n_zero, Z3_mk_select(ctx, u_a_ast, n_zero) );
d_v = Z3_mk_store(ctx, d_v, n_zero, Z3_mk_select(ctx, u_d_ast, n_zero) );
for (int i = 1; i< parameter; i++){
ind = Z3_mk_unsigned_int(ctx, i, bv32_sort);
ind_1 = Z3_mk_unsigned_int(ctx, i-1, bv32_sort);
check_old = Z3_mk_select(ctx, check_v , ind_1 );
d_v = Z3_mk_store(ctx, d_v, ind, Z3_mk_select(ctx, u_d_ast, pointer_d[i]) );
d_new = Z3_mk_select(ctx, d_v , ind );
pointer_d_plus_1 = Z3_mk_bvadd(ctx, pointer_d[i-1], n_one);
condition_d_pointer1[i] = Z3_mk_ge(ctx, Z3_mk_bv2int(ctx, pointer_d[i], false), Z3_mk_bv2int(ctx, pointer_d[i-1], false) );
condition_d_pointer2[i] = Z3_mk_le(ctx, Z3_mk_bv2int(ctx, pointer_d[i], false), Z3_mk_bv2int(ctx, pointer_d_plus_1, false) );
Z3_solver_assert(ctx, s, condition_d_pointer1[i]);
Z3_solver_assert(ctx, s, condition_d_pointer2[i]);
a_v = Z3_mk_store(ctx, a_v, ind, Z3_mk_select(ctx, u_a_ast, pointer_a[i]) );
a_new = Z3_mk_select(ctx, a_v , ind );
pointer_a_plus_1 = Z3_mk_bvadd(ctx, pointer_a[i-1], n_one);
condition_a_pointer1[i] = Z3_mk_ge(ctx, Z3_mk_bv2int(ctx, pointer_a[i], false), Z3_mk_bv2int(ctx, pointer_a[i-1], false) );
condition_a_pointer2[i] = Z3_mk_le(ctx, Z3_mk_bv2int(ctx, pointer_a[i], false), Z3_mk_bv2int(ctx, pointer_a_plus_1, false) );
Z3_solver_assert(ctx, s, condition_a_pointer1[i]);
Z3_solver_assert(ctx, s, condition_a_pointer2[i]);
d_xor_a = Z3_mk_bvxor(ctx, d_new , a_new);
check_new = Z3_mk_bvxor(ctx, check_old, d_xor_a);
check_v = Z3_mk_store(ctx, check_v, ind, check_new);
}
check3 = Z3_mk_select(ctx, check_v , n_position );
eq = Z3_mk_eq(ctx, n_ABCD, check3);
Z3_solver_assert(ctx, s, eq );
check(ctx, s, Z3_L_TRUE);
尝试使用 gdb 运行失败的实例时，它会给出以下消息：
Program received signal SIGSEGV, Segmentation fault.
0x00001blaab9fff68 in mpn_manager::div_normalize(unsigned int const*, unsigned long, unsigned int const*, unsigned long, mpn_manager::mpn_sbuffer&, mpn_manager::mpn_sbuffer&) const () from /lib/libz3.so
(gdb) backtrace
#0 0x00001blaab9ffd68 in mpn_manager::div_normalize(unsigned int const*, unsigned long, unsigned int const*, unsigned long, mpn_manager::mpn_sbuffer&, mpn_manager::mpn_sbuffer&) const () from /lib/libz3.so
#1 0x00001blaab9ffaf9 in mpn_manager::div(unsigned int const*, unsigned long, unsigned int const*, unsigned long, unsigned int*, unsigned int*) () from /lib/libz3.so
#2 0x00001blaab9e387e in void mpz_manager<true>::quot_rem_core<1>(mpz const&, mpz const&, mpz&, mpz&) () from /lib/libz3.so
#3 0x00001blaab9e4216 in mpz_manager<true>::rem(mpz const&, mpz const&, mpz&) () from /lib/libz3.so
#4 0x00001blaab9e4b71 in mpz_manager<true>::gcd(mpz const&, mpz const&, mpz&) () from /lib/libz3.so
#5 0x00001blaabdef04f in mpq_manager<true>::div(mpq const&, mpq const&, mpq&) () from /lib/libz3.so
#6 0x00001blaab139a0e in smt::theory_arith<smt::mi_ext>::update_and_pivot(int, int, rational const&, inf_rational const&) () from /lib/libz3.so
#7 0x00001blaab13a996 in smt::theory_arith<smt::mi_ext>::make_var_feasible(int) () from /lib/libz3.so
#8 0x00001blaab135aca in smt::theory_arith<smt::mi_ext>::make_feasible() () from /lib/libz3.so
#9 0x00001blaab136b13 in smt::theory_arith<smt::mi_ext>::propagate_core() () from /lib/libz3.so
#10 0x00001blaab22d9ad in smt::context::propagate() () from /lib/libz3.so
#11 0x00001blaab2328c0 in smt::context::bounded_search() () from /lib/libz3.so
#12 0x00001blaab231cd8 in smt::context::search() () from /lib/libz3.so
#13 0x00001blaab231b72 in smt::context::setup_and_check(bool) () from /lib/libz3.so
#14 0x00001blaaa10143f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#15 0x00001blaab665115 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#16 0x00001blaab65a333 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from /lib/libz3.so
#17 0x00001blaab65a5ad in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::string&) () from /lib/libz3.so
#18 0x00001blaab539703 in tactic2solver::check_sat_core(unsigned int, expr* const*) () from /lib/libz3.so
#19 0x00001blaab54208b in solver_na2as::check_sat(unsigned int, expr* const*) () from /lib/libz3.so
#20 0x00001blaab53d519 in combined_solver::check_sat(unsigned int, expr* const*) () from /lib/libz3.so
#21 0x00001blaaad73f8e in Z3_solver_check () from /lib/libz3.so
#22 0x0000000000402ce4 in check (ctx=0x622f48, s=0x66d948, expected_result=Z3_L_TRUE) at example.c:210
#23 0x0000000000405830 in main () at example.c:1129
如下所示： 使用 Z3 检查溢出似乎问题是由于Z3_mk_bv2int腐败造成的。当我使用mk_eq然后mk_or而不是这些小于/大于或等于时，（或使用gte，lte的bv版本;即Z3_mk_bvuge和Z3_mk_bvule）它适用于所有数字。