diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index fbe112e4c..dbf1252af 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7457,8 +7457,7 @@ def WithParams(t, p):
     >>> t((x + 1)*(y + 2) == 0)
     [[2*x + y + x*y == -2]]
     """
-    ctx = keys.pop('ctx', None)
-    t = _to_tactic(t, ctx)
+    t = _to_tactic(t, None)
     return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
 
 def Repeat(t, max=4294967295, ctx=None):
diff --git a/src/util/lp/eta_matrix.h b/src/util/lp/eta_matrix.h
index 7224fa846..89d2e641d 100644
--- a/src/util/lp/eta_matrix.h
+++ b/src/util/lp/eta_matrix.h
@@ -83,12 +83,12 @@ public:
     void apply_from_right(vector<T> & w) override;
     void apply_from_right(indexed_vector<T> & w) override;
 
-    T get_elem(unsigned i, unsigned j) const;
+    T get_elem(unsigned i, unsigned j) const override;
 #ifdef Z3DEBUG
-    unsigned row_count() const { return m_length; }
-    unsigned column_count() const { return m_length; }
-    void set_number_of_rows(unsigned m) { m_length = m; }
-    void set_number_of_columns(unsigned n) { m_length = n; }
+    unsigned row_count() const override { return m_length; }
+    unsigned column_count() const override { return m_length; }
+    void set_number_of_rows(unsigned m) override { m_length = m; }
+    void set_number_of_columns(unsigned n) override { m_length = n; }
 #endif
     void divide_by_diagonal_element() {
         m_column_vector.divide(m_diagonal_element);