From e4b660321f89cfda69d92ba8e52cc818a2e3e552 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Thu, 29 Apr 2021 16:16:48 -0700 Subject: [PATCH] Cpp api string const (#5228) * string_const added * typo fixed --- src/api/c++/z3++.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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)); }