Problem with conversion from bv to int.

Apr 18, 2014 at 8:36 AM
Hello.
I'm trying to convert bv to int using function Z3_mk_bv2int() with help of C++ API:
#include <iostream>
#include <z3/z3++.h>

int main(void) {
    using namespace z3;
    context ctx;
    auto bv = ctx.bv_val(1024, 32);
    Z3_context z3ctx = ctx;
    Z3_ast z3bv = bv;
    auto bv2int = Z3_mk_bv2int(z3ctx, z3bv, Z3_TRUE);
    auto integer = to_expr(ctx, bv2int);

    std::cout << bv << std::endl;
    std::cout << integer << std::endl;
}
But I'm getting Segmentation fault on function Z3_mk_bv2int. If I change Z3_TRUE to Z3_FALSE in function call (generate unsigned int) all works normally and no segmentation faults occurs.

I also tried to use pure C API and NO segmentation fault occurred in both cases with Z3_TRUE and with Z3_FALSE.
#include <stdio.h>
#include <z3/z3.h>

int main(void) {
    Z3_config config = Z3_mk_config();
    Z3_context context = Z3_mk_context(config);

    Z3_sort sort = Z3_mk_bv_sort(context, 32);
    Z3_ast bv = Z3_mk_int(context, 32, sort);

    Z3_ast integer = Z3_mk_bv2int(context, bv, 0); 

    Z3_set_ast_print_mode(context, Z3_PRINT_SMTLIB2_COMPLIANT);
    printf("bv: %s\n", Z3_ast_to_string(context, bv));
    printf("integer: %s\n", Z3_ast_to_string(context, integer));

    Z3_del_context(context);
    Z3_del_config(config);  
}
I'm working on 64-bit Linux.
Coordinator
Apr 20, 2014 at 12:09 PM
Edited Apr 20, 2014 at 12:09 PM
Thanks for reporting this problem! I can't replicate this on my system, are you using the latest code from the unstable branch? We fixed a very similar problem recently and I think this may have fixed your problem too (see here).
Apr 21, 2014 at 12:31 PM
Thanks for answer.
No, I'm using master branch. I will try to switch to unstable branch and check my problem.
Apr 28, 2014 at 8:17 AM
Yes, on the latest version of unstable everything works fine. Thank a lot!