CODEWITHSUNDEEP
z3
Heyji
Heyji

Reputation: 1211

Mixing Z3 c and c++ apis

Why does the following code not work ? I get a runtime error.

#include <iostream>
#include "z3++.h"

using namespace std;

int main()
{
    z3::context c;
    z3::expr a = c.bv_val(12,16);
    Z3_ast a0 = Z3_mk_extract(a.ctx(),0,0,a);
    Z3_ast a1 = Z3_mk_extract(a.ctx(),1,1,a);
    Z3_ast a2 = Z3_mk_extract(a.ctx(),2,2,a);
    cout << Z3_ast_to_string(a.ctx(),a0);
    cout << Z3_ast_to_string(a.ctx(),a1);  // <-- BOOM
    cout << Z3_ast_to_string(a.ctx(),a2);
}

if i only use the C api, it works perfectly. I thought i could mix the two api easily...

A.G.

Upvotes: 2

Views: 237

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8369

From the C API functions, such as Z3_mk_extract, you have to maintain reference counters on created objects yourself. The C++ wrapper automatically increases a reference counts in the "expr" class. So one way of fixing the code is to wrap a0, a1, a2 in exprs. E.g., you can say:

 z3::expr a0 = z3::expr(c, Z3_mk_extract(a.ctx(),0,0,a));

Upvotes: 3

Related Questions