diff --git a/src/sat/smt/arith_proof_checker.h b/src/sat/smt/arith_proof_checker.h
index 2333d1e3b56..0f223081b2e 100644
--- a/src/sat/smt/arith_proof_checker.h
+++ b/src/sat/smt/arith_proof_checker.h
@@ -397,7 +397,7 @@ namespace arith {
             return false;
         }
 
-        void register_plugins(euf::proof_checker& pc) {
+        void register_plugins(euf::proof_checker& pc) override {
             pc.register_plugin(symbol("farkas"), this);
             pc.register_plugin(symbol("bound"), this);
             pc.register_plugin(symbol("implied-eq"), this);
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 4ec90166a33..14671d55af4 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -176,7 +176,7 @@ namespace euf {
         display_literals(out << "(assume", n, lits) << ")\n";        
     }
 
-    void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr_ref& proof_hint) {
+    void solver::display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint) {
         if (proof_hint)
             visit_expr(out, proof_hint);
         display_hint(display_literals(out << "(learn", n, lits), proof_hint) << ")\n";        
diff --git a/src/sat/smt/euf_proof_checker.cpp b/src/sat/smt/euf_proof_checker.cpp
index 9943c57299d..38ad62589b7 100644
--- a/src/sat/smt/euf_proof_checker.cpp
+++ b/src/sat/smt/euf_proof_checker.cpp
@@ -26,6 +26,7 @@ namespace euf {
         arith::proof_checker* apc = alloc(arith::proof_checker, m);
         m_plugins.push_back(apc);
         apc->register_plugins(*this);
+        (void)m;
     }
 
     proof_checker::~proof_checker() {}
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 71569676a20..91b348e5002 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -184,7 +184,7 @@ namespace euf {
         void on_proof(unsigned n, literal const* lits, sat::status st);
         std::ostream& display_literals(std::ostream& out, unsigned n, sat::literal const* lits);
         void display_assume(std::ostream& out, unsigned n, literal const* lits);
-        void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr_ref& proof_hint);        
+        void display_redundant(std::ostream& out, unsigned n, literal const* lits, expr* proof_hint);        
         void display_deleted(std::ostream& out, unsigned n, literal const* lits);
         std::ostream& display_hint(std::ostream& out, expr* proof_hint);
         expr_ref status2proof_hint(sat::status st);