diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 95b01979e..44972565e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -84,8 +84,9 @@ namespace z3 { std::string m_msg; public: exception(char const * msg):m_msg(msg) {} + virtual ~exception() throw() {} char const * msg() const { return m_msg.c_str(); } - char const * what() const noexcept { return m_msg.c_str(); } + char const * what() const throw() { return m_msg.c_str(); } friend std::ostream & operator<<(std::ostream & out, exception const & e); }; inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; } @@ -2784,7 +2785,8 @@ namespace z3 { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); add(expr_vector(c, src.assertions())); - for (expr const& o : expr_vector(c, src.objectives())) minimize(o); + expr_vector v(c, src.objectives()); + for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it); } optimize& operator=(optimize const& o) { Z3_optimize_inc_ref(o.ctx(), o.m_opt); @@ -2800,7 +2802,7 @@ namespace z3 { Z3_optimize_assert(ctx(), m_opt, e); } void add(expr_vector const& es) { - for (expr const& e : es) add(e); + for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it); } handle add(expr const& e, unsigned weight) { assert(e.is_bool());