mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add missing inline fix #1917
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f699ac0353
commit
1a030bb722
|
@ -2847,7 +2847,7 @@ namespace z3 {
|
|||
return recfun(str_symbol(name), 2, dom, range);
|
||||
}
|
||||
|
||||
void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
|
||||
inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
|
||||
check_context(f, args); check_context(f, body);
|
||||
array<Z3_ast> vars(args);
|
||||
Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
|
||||
|
|
Loading…
Reference in a new issue