From a8ccbd7103f193c574ba3d0f2ef45edb1bf9fe66 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Apr 2021 13:36:25 -0700 Subject: [PATCH] fix #5226 --- src/api/c++/z3++.h | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 24547891e..7e6a7afe6 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2984,8 +2984,16 @@ namespace z3 { return *this; } operator Z3_fixedpoint() const { return m_fp; } - void from_string(char const* s) { Z3_fixedpoint_from_string(ctx(), m_fp, s); check_error(); } - void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); } + expr_vector from_string(char const* s) { + Z3_ast_vector r = Z3_fixedpoint_from_string(ctx(), m_fp, s); + check_error(); + return expr_vector(ctx(), r); + } + expr_vector from_file(char const* s) { + Z3_ast_vector r = Z3_fixedpoint_from_file(ctx(), m_fp, s); + check_error(); + return expr_vector(ctx(), r); + } void add_rule(expr& rule, symbol const& name) { Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); } void add_fact(func_decl& f, unsigned * args) { Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); } check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); }