From 9cf50766a636050da7731bd58dcd01219cbe744b Mon Sep 17 00:00:00 2001 From: Qix Date: Wed, 16 Feb 2022 22:36:34 +0100 Subject: [PATCH] fix compiler warnings under clang (#5839) --- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/sat/smt/pb_solver.cpp | 2 +- src/smt/theory_lra.cpp | 1 + src/tactic/core/collect_statistics_tactic.cpp | 1 - 4 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 86de919dc..db1f28743 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -687,7 +687,7 @@ public: return ensure_euf()->user_propagate_register_expr(e); } - void user_propagate_register_created(user_propagator::created_eh_t& r) { + void user_propagate_register_created(user_propagator::created_eh_t& r) override { ensure_euf()->user_propagate_register_created(r); } diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 5e63f19ad..62e3c88fb 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -1458,7 +1458,7 @@ namespace pb { return nullptr; } rational weight(0); - for (auto const [w, l] : wlits) + for (auto const &[w, l] : wlits) weight += w; if (weight < k) { if (lit == sat::null_literal) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c89628808..65e51fe03 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1563,6 +1563,7 @@ public: return FC_CONTINUE; } for (expr* e : m_not_handled) { + (void) e; // just in case TRACE() is a no-op TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";); st = FC_GIVEUP; } diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index 5c7ec827c..dc906cb32 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -110,7 +110,6 @@ protected: void operator()(quantifier * q) { m_stats["quantifiers"]++; SASSERT(is_app(q->get_expr())); - app * body = to_app(q->get_expr()); switch (q->get_kind()) { case forall_k: m_stats["forall-variables"] += q->get_num_decls();