mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

check-error

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-21 02:44:53 -07:00
parent d27527d4df
commit f86a9b4b70
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/c++/z3++.h
View file

@ -1941,8 +1941,8 @@ namespace z3 {
} }
// fails for some compilers: // fails for some compilers:
// void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); } // 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_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); ctx().check_parser_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() { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
check_result check(unsigned n, expr * const assumptions) { check_result check(unsigned n, expr * const assumptions) {
array<Z3_ast> _assumptions(n); array<Z3_ast> _assumptions(n);