From ce67c8277c62b10cbb295266c0c6cc939dc86910 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 24 Apr 2017 12:59:44 +0000 Subject: [PATCH] Return check result in fixedpoint object This is a small change to fix a missing return statement. --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b6157f3ff..9d9982523 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2244,7 +2244,7 @@ namespace z3 { void from_file(char const* s) { Z3_fixedpoint_from_file(ctx(), m_fp, s); check_error(); } 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(); to_check_result(r); } + check_result query(expr& q) { Z3_lbool r = Z3_fixedpoint_query(ctx(), m_fp, q); check_error(); return to_check_result(r); } check_result query(func_decl_vector& relations) { array rs(relations); Z3_lbool r = Z3_fixedpoint_query_relations(ctx(), m_fp, rs.size(), rs.ptr());