diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 270a98ca9..de239a804 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1939,8 +1939,10 @@ namespace z3 {
         void add(expr const & e, char const * p) {
             add(e, ctx().bool_const(p));
         }
-        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); check_error(); }
+        // 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(); }
         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<Z3_ast> _assumptions(n);
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 08b771df5..1b99cf0df 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -711,7 +711,7 @@ public:
         m_imp = alloc(imp, m, p, r, owner);
     }
 
-    virtual tactic * translate(ast_manager & m) {
+    tactic * translate(ast_manager & m) override {
         return alloc(solve_eqs_tactic, m, m_params, mk_expr_simp_replacer(m, m_params), true);
     }
         
@@ -719,12 +719,12 @@ public:
         dealloc(m_imp);
     }
 
-    virtual void updt_params(params_ref const & p) {
+    void updt_params(params_ref const & p) override {
         m_params = p;
         m_imp->updt_params(p);
     }
 
-    virtual void collect_param_descrs(param_descrs & r) {
+    void collect_param_descrs(param_descrs & r) override {
         r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
         r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
         r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
@@ -736,7 +736,7 @@ public:
         report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
     }
     
-    virtual void cleanup() {
+    void cleanup() override {
         unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
         ast_manager & m = m_imp->m();
         expr_replacer * r = m_imp->m_r;
@@ -751,11 +751,11 @@ public:
         dealloc(d);
     }
 
-    virtual void collect_statistics(statistics & st) const {
+    void collect_statistics(statistics & st) const override {
         st.update("eliminated vars", m_imp->get_num_eliminated_vars());
     }
 
-    virtual void reset_statistics() {
+    void reset_statistics() override {
         m_imp->m_num_eliminated_vars = 0;
     }