build fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 29, 2022 · dd90689 · dd90689
1 parent 6f2a6da
commit dd90689
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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);