mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

#5484

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-16 11:19:22 -07:00
parent 904c6e21b1
commit c8a83749dd
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/api_ast.cpp
View file

@ -137,6 +137,11 @@ extern "C" {
func_decl* d = to_func_decl(f); func_decl* d = to_func_decl(f);
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin(); recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
if (!p.has_def(d)) {
std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl";
SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
return;
}
expr_ref abs_body(m); expr_ref abs_body(m);
expr_ref_vector _args(m); expr_ref_vector _args(m);
var_ref_vector _vars(m); var_ref_vector _vars(m);

3
src/ast/ast_pp.h
View file

@ -67,4 +67,7 @@ inline std::string operator+(std::string const& s, mk_pp const& pp) {
return strm.str(); return strm.str();
} }
inline std::string& operator+=(std::string& s, mk_pp const& pp) {
return s = s + pp;
}