diff --git a/src/ast/simplifier/poly_simplifier_plugin.h b/src/ast/simplifier/poly_simplifier_plugin.h
index 66ecf4bb0..ec4aa336e 100644
--- a/src/ast/simplifier/poly_simplifier_plugin.h
+++ b/src/ast/simplifier/poly_simplifier_plugin.h
@@ -134,6 +134,10 @@ public:
     virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
 
     virtual bool reduce(func_decl * f, unsigned num_args, rational const * mults, expr * const * args, expr_ref & result);
+    virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+        return simplifier_plugin::reduce(f, num_args, args, result);
+    }
+
 
     expr * get_monomial_body(expr * m);
     int get_monomial_body_order(expr * m);
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 36b1dcd51..76ad2a020 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -181,6 +181,7 @@ class paccessor_decl : public pdecl {
     ptype const & get_type() const { return m_type; }
     virtual ~paccessor_decl() {}
 public:
+    virtual void display(std::ostream & out) const { pdecl::display(out); }
     void display(std::ostream & out, pdatatype_decl const * const * dts) const;
 };
 
@@ -201,6 +202,7 @@ class pconstructor_decl : public pdecl {
     constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s);
     virtual ~pconstructor_decl() {}
 public:
+    virtual void display(std::ostream & out) const { pdecl::display(out); }
     void display(std::ostream & out, pdatatype_decl const * const * dts) const;
 };
 
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 71b59ac26..1a6a3f9c6 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -270,7 +270,7 @@ namespace pdr {
                 (*this)(n, new_cores.back().first, new_cores.back().second);
             }
         }
-        virtual void collect_statistics(statistics& st) {}
+        virtual void collect_statistics(statistics& st) const {}
     };
 
     class context {
diff --git a/src/smt/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp
index 86351e36f..a68b7782b 100644
--- a/src/smt/theory_diff_logic.cpp
+++ b/src/smt/theory_diff_logic.cpp
@@ -22,9 +22,11 @@ Revision History:
 #include"rational.h"
 #include"theory_diff_logic_def.h"
 
+namespace smt {
 
 template class theory_diff_logic<idl_ext>;
 template class theory_diff_logic<sidl_ext>;
 template class theory_diff_logic<rdl_ext>;
 template class theory_diff_logic<srdl_ext>;
 
+};