diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp
index e99568961..c2efb520d 100644
--- a/src/ast/rewriter/expr_safe_replace.cpp
+++ b/src/ast/rewriter/expr_safe_replace.cpp
@@ -19,6 +19,7 @@ Revision History:
 --*/
 
 #include "ast/rewriter/expr_safe_replace.h"
+#include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
 
 
diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h
index 3c7be4742..fb66661af 100644
--- a/src/ast/rewriter/expr_safe_replace.h
+++ b/src/ast/rewriter/expr_safe_replace.h
@@ -23,7 +23,6 @@ Revision History:
 #define EXPR_SAFE_REPLACE_H_
 
 #include "ast/ast.h"
-#include "ast/rewriter/var_subst.h"
 
 class expr_safe_replace {
     ast_manager& m;
diff --git a/src/ast/rewriter/recfun_replace.h b/src/ast/rewriter/recfun_replace.h
index 78dd0ee56..5a24e8513 100644
--- a/src/ast/rewriter/recfun_replace.h
+++ b/src/ast/rewriter/recfun_replace.h
@@ -34,8 +34,8 @@ class recfun_replace : public recfun::replace {
 public:
     recfun_replace(ast_manager& m): m(m), m_replace(m) {}
     void reset() override { m_replace.reset(); }
-    void insert(expr* s, expr* t) { m_replace.insert(s, t); }
-    expr_ref operator()(expr* e) { expr_ref r(m); m_replace(e, r); return r; }
+    void insert(expr* s, expr* t) override { m_replace.insert(s, t); }
+    expr_ref operator()(expr* e) override { expr_ref r(m); m_replace(e, r); return r; }
 };
 
 #endif /* RECFUN_REPLACE_H_ */