diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 7e6a7afe6..8d0e4d037 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -335,6 +335,7 @@ namespace z3 { expr bool_const(char const * name); expr int_const(char const * name); expr real_const(char const * name); + expr string_const(char const * name); expr bv_const(char const * name, unsigned sz); expr fpa_const(char const * name, unsigned ebits, unsigned sbits); @@ -895,7 +896,7 @@ namespace z3 { */ expr mk_to_ieee_bv() const { assert(is_fpa()); - Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast), + Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast); check_error(); return expr(ctx(), r); } @@ -3231,6 +3232,7 @@ namespace z3 { inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); } inline expr context::int_const(char const * name) { return constant(name, int_sort()); } inline expr context::real_const(char const * name) { return constant(name, real_sort()); } + inline expr context::string_const(char const * name) { return constant(name, string_sort()); } inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); } inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }