3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

addrecdef

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-04 18:18:25 -07:00
parent 51d43c04ea
commit 74eb401c3b

View file

@ -347,7 +347,7 @@ end = struct
let mk_rec_fun_s (ctx:context) (name:string) (domain:Sort.sort list) (range:Sort.sort) =
mk_rec_fun ctx (Symbol.mk_string ctx name) domain range
let add_rec_def (ctx:context) (f:func_decl) (args:Expr.expr list) (body:Expr.expr)
let add_rec_def (ctx:context) (f:func_decl) (args:Expr.expr list) (body:Expr.expr) =
Z3native.add_rec_def ctx f (List.length args) args body
let mk_fresh_func_decl (ctx:context) (prefix:string) (domain:Sort.sort list) (range:Sort.sort) =