I have written a Z3 program (starting from test_capi.c) that loops on some number "parameter" and adds constraints for each loop cycle, that are dependent on the previous loop's constraints. The idea is that each cycle 2 items a,d are selected which would be either the same old a,d or new a,d picked by pointer_a, pointer_d from ordered lists u_a, u_d.
The code works for some loop counts and not for others (gives sat versus a segmentation fault). More strange, the numbers of the loop counts for which the code works changes when changing the code. So the code below works and is SAT (I already picked n_ABCD=check3 ), but it gives the result only for "parameter" from 2 up to 10, except for 6, and for parameter=8, 16, 32 and could be some other numbers, but I tried those at least; it didn't work for 31, 33, 64, 128 and 512. When I split the loop into 2 loops one for the pointer_a[] & pointer_d[] constraints, and the other for the check_v manipulation the code works for "parameter" up to 9, and then for 12, 14, 17 and 27 & I've not been lucky with other bigger numbers. The goal was to run it up to parameter=1024 or even more.
Any explanation of why could the code be running only for some numbers and not for others? Is it related to how the selection of the arbitrary terms being evaluated works? (make_var_feasible, update_and_pivot ... as in the gdb trace more below)
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);
Trying to run a failing instance with gdb, it gives the following message:
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
As in here: Check overflow with Z3 Seems the problem is due to Z3_mk_bv2int corruption. When I used mk_eq and then mk_or instead of these less-than/greater-than than or equal, (or using the bv version of gte, lte; i.e. Z3_mk_bvuge & Z3_mk_bvule) it works fine for all numbers.