diff --git a/src/ast/converters/equiv_proof_converter.h b/src/ast/converters/equiv_proof_converter.h index 7f98d1e0c..9f5eac10c 100644 --- a/src/ast/converters/equiv_proof_converter.h +++ b/src/ast/converters/equiv_proof_converter.h @@ -44,6 +44,6 @@ public: ast_manager& get_manager() { return m; } - void display(std::ostream & out) override {} + void display(std::ostream &) override { } }; diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h index e176243c0..630159e3e 100644 --- a/src/ast/converters/generic_model_converter.h +++ b/src/ast/converters/generic_model_converter.h @@ -50,7 +50,7 @@ public: void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); } - void operator()(labels_vec & labels) override {} + void operator()(labels_vec &) override { } void operator()(model_ref & md) override; diff --git a/src/ast/converters/horn_subsume_model_converter.h b/src/ast/converters/horn_subsume_model_converter.h index 2576ad1f9..e5fd1cef7 100644 --- a/src/ast/converters/horn_subsume_model_converter.h +++ b/src/ast/converters/horn_subsume_model_converter.h @@ -76,7 +76,7 @@ public: ast_manager& get_manager() { return m; } - void display(std::ostream & out) override {} + void display(std::ostream &) override { } void get_units(obj_map& units) override { units.reset(); } diff --git a/src/ast/converters/replace_proof_converter.h b/src/ast/converters/replace_proof_converter.h index 6a877bc58..3ab82fd6f 100644 --- a/src/ast/converters/replace_proof_converter.h +++ b/src/ast/converters/replace_proof_converter.h @@ -42,7 +42,7 @@ public: // run the replacements the inverse direction. void invert() { m_proofs.reverse(); } - void display(std::ostream & out) override {} + void display(std::ostream &) override { } }; diff --git a/src/ast/euf/euf_arith_plugin.h b/src/ast/euf/euf_arith_plugin.h index fddb951dd..9d7471229 100644 --- a/src/ast/euf/euf_arith_plugin.h +++ b/src/ast/euf/euf_arith_plugin.h @@ -39,7 +39,7 @@ namespace euf { void merge_eh(enode* n1, enode* n2) override; - void diseq_eh(enode* eq) override {} + void diseq_eh(enode*) override { } void undo() override; diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h index 6bf48df2a..d86be621d 100644 --- a/src/ast/euf/euf_bv_plugin.h +++ b/src/ast/euf/euf_bv_plugin.h @@ -101,7 +101,7 @@ namespace euf { void merge_eh(enode* n1, enode* n2) override; - void diseq_eh(enode* eq) override {} + void diseq_eh(enode*) override { } void propagate() override; diff --git a/src/ast/sls/sls_array_plugin.h b/src/ast/sls/sls_array_plugin.h index ca72a454e..8bc3de45a 100644 --- a/src/ast/sls/sls_array_plugin.h +++ b/src/ast/sls/sls_array_plugin.h @@ -122,7 +122,7 @@ namespace sls { void propagate_literal(sat::literal lit) override { m_g = nullptr; } bool propagate() override { return false; } bool repair_down(app* e) override { return true; } - void repair_up(app* e) override {} + void repair_up(app*) override { } void repair_literal(sat::literal lit) override { m_g = nullptr; } bool is_sat() override; diff --git a/src/ast/sls/sls_basic_plugin.h b/src/ast/sls/sls_basic_plugin.h index 6c1936532..1c263884e 100644 --- a/src/ast/sls/sls_basic_plugin.h +++ b/src/ast/sls/sls_basic_plugin.h @@ -51,7 +51,7 @@ namespace sls { void on_restart() override {} std::ostream& display(std::ostream& out) const override; bool set_value(expr* e, expr* v) override; - void collect_statistics(statistics& st) const override {} + void collect_statistics(statistics&) const override { } void reset_statistics() override {} }; diff --git a/src/ast/sls/sls_datatype_plugin.h b/src/ast/sls/sls_datatype_plugin.h index 0507c68c0..5c0310e43 100644 --- a/src/ast/sls/sls_datatype_plugin.h +++ b/src/ast/sls/sls_datatype_plugin.h @@ -92,7 +92,7 @@ namespace sls { void register_term(expr* e) override; bool set_value(expr* e, expr* v) override { return false; } - void repair_literal(sat::literal lit) override {} + void repair_literal(sat::literal) override { } bool include_func_interp(func_decl* f) const override; bool check_ackerman(func_decl* f) const override; diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h index 2c465e66f..1520f7736 100644 --- a/src/ast/sls/sls_euf_plugin.h +++ b/src/ast/sls/sls_euf_plugin.h @@ -72,9 +72,9 @@ namespace sls { bool set_value(expr* e, expr* v) override { return false; } bool include_func_interp(func_decl* f) const override; - void repair_up(app* e) override {} + void repair_up(app*) override { } bool repair_down(app* e) override { return false; } - void repair_literal(sat::literal lit) override {} + void repair_literal(sat::literal) override { } void collect_statistics(statistics& st) const override; void reset_statistics() override; diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index 5914e17ab..48eb4721c 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -185,7 +185,7 @@ namespace sls { bool repair_down(app* e) override; void repair_literal(sat::literal lit) override; - void collect_statistics(statistics& st) const override {} + void collect_statistics(statistics&) const override { } void reset_statistics() override {} }; diff --git a/src/model/fpa_factory.h b/src/model/fpa_factory.h index 1c2c98b25..83b1dad07 100644 --- a/src/model/fpa_factory.h +++ b/src/model/fpa_factory.h @@ -62,7 +62,7 @@ class fpa_value_factory : public value_factory { } expr * get_fresh_value(sort * s) override { return get_some_value(s); } - void register_value(expr * n) override { /* Ignore */ } + void register_value(expr *) override { /* Ignore */ } app * mk_value(mpf const & x) { return m_util.mk_value(x); diff --git a/src/model/value_factory.h b/src/model/value_factory.h index 85515495b..94ffc8bad 100644 --- a/src/model/value_factory.h +++ b/src/model/value_factory.h @@ -70,7 +70,7 @@ public: expr * get_fresh_value(sort * s) override; - void register_value(expr * n) override { } + void register_value(expr *) override { } }; /** diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index edf24d9bb..7e75cde45 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -97,7 +97,7 @@ namespace opt { rational get_lower() const override { return m_lower; } rational get_upper() const override { return m_upper; } bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); } - void collect_statistics(statistics& st) const override { } + void collect_statistics(statistics&) const override { } void get_model(model_ref& mdl, svector& labels) override { mdl = m_model.get(); labels = m_labels;} virtual void commit_assignment(); void set_model() { s().get_model(m_model); s().get_labels(m_labels); } diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 1daed0e3b..0ee8c390f 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -121,11 +121,11 @@ public: m_opt(opt) {} - void reset(cmd_context & ctx) override { } + void reset(cmd_context &) override { } char const * get_usage() const override { return ""; } char const * get_descr(cmd_context & ctx) const override { return "check sat modulo objective function";} unsigned get_arity() const override { return 1; } - void prepare(cmd_context & ctx) override {} + void prepare(cmd_context &) override { } cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; } void set_next_arg(cmd_context & ctx, expr * t) override { @@ -152,11 +152,11 @@ public: m_opt(opt) {} - void reset(cmd_context & ctx) override { } + void reset(cmd_context &) override { } char const * get_usage() const override { return "(get-objectives)"; } char const * get_descr(cmd_context & ctx) const override { return "retrieve the objective values (after optimization)"; } unsigned get_arity() const override { return 0; } - void prepare(cmd_context & ctx) override {} + void prepare(cmd_context &) override { } void failure_cleanup(cmd_context & ctx) override {