diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 52cce7437..382bc9d3e 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -221,7 +221,7 @@ namespace {
             return m_context.user_propagate_register(e);
         }
 
-        void user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq) {
+        void user_propagate_consequence(unsigned sz, unsigned const* ids, expr* conseq) override {
             m_context.user_propagate_consequence(sz, ids, conseq);
         }        
 
diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h
index b27a6aa93..208e94473 100644
--- a/src/smt/user_propagator.h
+++ b/src/smt/user_propagator.h
@@ -97,6 +97,6 @@ namespace smt {
         bool include_func_interp(func_decl* f) override { return false; }
         bool can_propagate() override;
         void propagate() override; 
-        void display(std::ostream& out) const {}
+        void display(std::ostream& out) const override {}
     };
 };