SegmentationFault using pop command and CharAt

[yannicnoller]

Hi all,

I tried to extend your code for some programmatically constraint assertions including the push and pop commands of the solver and the call of the CharAt function. I tried to break the code down to the actual problem and put everything at the end of the pa_theory_example method to keep things simple. After the first pop call, the CharAt function call is resulting in a Segmentation fault. But I can do other assertions like equal or calling the Length function without geetting a segfault. I have no idea what I'm doing wrong or whether it's a bug of Z3. I appreciate any help.

Thanks, Yannic

The input file:

(declare-const x String)
(set-option :produce-models true)

(declare-const __cOnStStR__x61 String)
(declare-const __cOnStStR__x7a String)

(assert (RegexIn x (RegexStar (RegexCharRange __cOnStStR__x61 __cOnStStR__x7a))))
(check-sat)

My code extension:

// Additional code to do some assertions programmatically.
Z3_model m = 0;
Z3_lbool result = Z3_check_and_get_model(ctx, &m);
if (result == Z3_L_TRUE) {

    // 1. Get Z3_ast object for variable "x".
    unsigned num_constants = Z3_get_model_num_constants(ctx, m);
    Z3_ast x = NULL;
    for (unsigned i = 0; i < num_constants; i++) {
        Z3_func_decl cnst = Z3_get_model_constant(ctx, m, i);
        Z3_symbol name = Z3_get_decl_name(ctx, cnst);
        Z3_ast a = Z3_mk_app(ctx, cnst, 0, 0);
        Z3_ast v = a;
        Z3_eval(ctx, m, a, &v);
        x = a;
        if (strcmp(Z3_get_symbol_string(ctx, name), "x") == 0) {
            break;
        }
    }
    Z3_del_model(ctx, m);
    m = 0;

    if (x != NULL) {

        PATheoryData * td = (PATheoryData *)Z3_theory_get_ext_data(Th);
        Z3_ast string_for_a = Z3_theory_mk_value(ctx, Th, Z3_mk_string_symbol(ctx, "__cOnStStR__x61"), td->String);
        Z3_ast string_for_b = Z3_theory_mk_value(ctx, Th, Z3_mk_string_symbol(ctx, "__cOnStStR__x62"), td->String);

        // 2. Assert CharAt(x, 0) = "a" and check SAT.
        Z3_push(ctx);
        Z3_ast newConstraint1 = Z3_mk_eq(ctx, mk_2_arg_app(ctx, td->CharAt, x, mk_int(ctx, 0)), string_for_a);
        display_ast(Th, stdout, 0, newConstraint1);
        Z3_assert_cnstr(ctx, newConstraint1);
        if (Z3_check(ctx) == Z3_L_TRUE)
            printf(" -> SAT\n");
        else 
            printf(" -> UNSAT\n");
        Z3_pop(ctx, 1);

        // 3. Assert CharAt(x, 0) = "b" and check SAT.
        Z3_push(ctx);
        Z3_ast newConstraint2 = Z3_mk_eq(ctx, mk_2_arg_app(ctx, td->CharAt, x, mk_int(ctx, 0)), string_for_b);
        display_ast(Th, stdout, 0, newConstraint2);
        Z3_assert_cnstr(ctx, newConstraint2);
        if (Z3_check(ctx) == Z3_L_TRUE)
            printf(" -> SAT\n");
        else
            printf(" -> UNSAT\n");
        Z3_pop(ctx, 1);
    }
    else {
        printf(">>>>>> x NOT FOUND !!!!!!\n");
    }
}

// clean up
Z3_del_context(ctx);

The output:

...
************************
(= (CharAt x 0) __cOnStStR__x61) -> SAT
WARNING: invalid function application, sort mismatch on argument at position 1
Segmentation fault (core dumped)