segmentation fault when creating constant in c++ api about z3 HOT 4 CLOSED

Resolved on stackoverflow.

from z3.

I don't see why this resolves the problem:
a) I still can't create an uninterpreted sort in the C++ API,
b) a segmentation fault is not the expected behaviour.

Ad a).
I suggest adding the following code to z3++.h (which works for me):

(line 181):

        /**
           \brief Create an uninterpreted sort with given symbol
        */
        sort uninterpreted_sort(char const * s);                

(line 1564):

    inline sort context::uninterpreted_sort(char const *name) { 
        Z3_symbol r = Z3_mk_string_symbol(m_ctx, name); check_error();
        Z3_sort s = Z3_mk_uninterpreted_sort(m_ctx, r); check_error(); return sort(*this, s); }

from z3.

Yes, you can create an uninterpreted sort in the C++ API, in exactly the way that you describe. (Your sort(*this, s) is what I call wrapping in z3::sort(ctx, ...)).

The C++ API is not intended to be a fully featured abstraction layer type of API, it's a thin layer on top of the C API that hides the reference counting mechanism for the various object types. For every other purpose, the functions from the C API can be used unmodified.

from z3.

The C++ API is not intended to be a fully featured abstraction layer type
of API, it's a thin layer on top of the C API that hides the reference
counting mechanism for the various object types. For every other purpose,
the functions from the C API can be used unmodified.

Thanks for the explanation, now I get it.

—
Reply to this email directly or view it on GitHub
#40 (comment).

from z3.