From 56827d572519524b940785c4e377e93297b768d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Apr 2018 23:10:21 -0700 Subject: [PATCH] adding the orphaned shorthand #1574 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 0ddebf75c..b81927474 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2680,9 +2680,12 @@ namespace z3 { inline func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) { return range.ctx().function(name, d1, d2, d3, d4, d5, range); } - inline func_decl function(char const& name, sort_vector const& domain, sort const& range) { + inline func_decl function(char const* name, sort_vector const& domain, sort const& range) { return range.ctx().function(name, domain, range); } + inline func_decl function(std::string const& name, sort_vector const& domain, sort const& range) { + return range.ctx().function(name.c_str(), domain, range); + } inline expr select(expr const & a, expr const & i) { check_context(a, i);