From f86a9b4b70a3972da1a9be13d203e7878bce7907 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Mar 2018 02:44:53 -0700 Subject: [PATCH] check-error Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index de239a804..adc5bbbcf 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1941,8 +1941,8 @@ namespace z3 { } // fails for some compilers: // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); } - void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); } - void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); } + void from_file(char const* file) { Z3_solver_from_file(ctx(), m_solver, file); check_error(); } + void from_string(char const* s) { Z3_solver_from_string(ctx(), m_solver, s); check_error(); } check_result check() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); } check_result check(unsigned n, expr * const assumptions) { array _assumptions(n);