Universal quantifiers with arrays as bound variables (C API)

[daneshvar-amrollahi]

Hi,

I have a benchmark including a universal quantifier over an array as the bound variable, implemented using the C API of Z3 as follows:

Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg);
Z3_solver theSolver = mk_solver(ctx);

Z3_sort domainSort = Z3_mk_bv_sort(ctx, 32);
Z3_sort rangeSort = Z3_mk_bv_sort(ctx, 8);
Z3_sort arr_sort = Z3_mk_array_sort(ctx, domainSort, rangeSort);

Z3_symbol arr_name = Z3_mk_string_symbol(ctx, "fqv");
Z3_ast fqv_arr = Z3_mk_const(ctx, arr_name, arr_sort);

Z3_ast idx = Z3_mk_concat(
        ctx, 
        Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 1, domainSort)),
        Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 0, domainSort))
    );
idx = Z3_mk_concat(ctx, Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 2, domainSort)), idx);
idx = Z3_mk_concat(ctx, Z3_mk_select(ctx, fqv_arr, Z3_mk_int(ctx, 3, domainSort)), idx);

arr_name = Z3_mk_string_symbol(ctx, "a");
Z3_ast a_arr = Z3_mk_const(ctx, arr_name, arr_sort);

arr_name = Z3_mk_string_symbol(ctx, "b");
Z3_ast b_arr = Z3_mk_const(ctx, arr_name, arr_sort);

Z3_ast body = Z3_mk_eq(ctx, Z3_mk_select(ctx, a_arr, idx), Z3_mk_select(ctx, b_arr, idx));

Z3_app bound_vars[] = {(Z3_app) fqv_arr};
int num_bound_vars = 1;
int weight = 0;
Z3_ast forall = Z3_mk_forall_const(ctx, weight, num_bound_vars, bound_vars, 0, 0, body);

Z3_ast a0 = Z3_mk_select(ctx, a_arr, Z3_mk_int(ctx, 0, domainSort));
Z3_ast b0 = Z3_mk_select(ctx, b_arr, Z3_mk_int(ctx, 0, domainSort));

Z3_solver_assert(ctx, theSolver, forall);
Z3_solver_assert(ctx, theSolver, Z3_mk_eq(ctx, Z3_mk_false(ctx), Z3_mk_eq(ctx, a0, b0)));

This benchmark is basically adding two constraints to the solver which are:

1. ∀fqv: a[fqv] = b[fqv]
2. a[0] != b[0]

with the following Z3_ast's:

 (forall ((fqv (Array (_ BitVec 32) (_ BitVec 8))))
  (! (= (select a
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000)))))
        (select b
                (concat (select fqv #x00000003)
                        (concat (select fqv #x00000002)
                                (concat (select fqv #x00000001)
                                        (select fqv #x00000000))))))
     :weight 0))

(= false (= (select a #x00000000) (select b #x00000000)))

fqv is also constrained to be between 0 and the size of the arrays.

The result that I am getting out of Z3_solver_check(ctx, theSolver) is Z3_L_UNDEF. However, I am expecting to get Z3_L_FALSE, since consraint 1 and 2 cannot hold at the same time.
Also, when I comment out the second constraint (a[0] != b[0]), it returns Z3_L_TRUE as expected.

Is there a way to make Z3 deal with the example above (to return Z3_L_FALSE instead of Z3_L_UNDEF)? Should I use patterns, or is there also some other way?