From d818233063682d8ee83f14496f516774063ad1e8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 23:21:48 -0700
Subject: [PATCH] unused variable warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq_offset_eq.cpp         | 5 +++--
 src/smt/theory_seq.cpp            | 4 +++-
 src/smt/theory_seq.h              | 2 +-
 src/tactic/ufbv/ufbv_rewriter.cpp | 1 -
 4 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/smt/seq_offset_eq.cpp b/src/smt/seq_offset_eq.cpp
index 7c02f611c39..10b34a8ef54 100644
--- a/src/smt/seq_offset_eq.cpp
+++ b/src/smt/seq_offset_eq.cpp
@@ -32,8 +32,9 @@ update m_offset_equalities to contain.
   r1 |-> [r2 |-> val]
 */
 
-seq_offset_eq::seq_offset_eq(theory& th, ast_manager& m): 
-    th(th), m(m), seq(m), a(m), m_propagation_level(-1) {
+seq_offset_eq::seq_offset_eq(theory& th, ast_manager& _m): 
+    th(th), m(_m), seq(m), a(m), m_propagation_level(-1) {
+    (void)m;
 }
 
 bool seq_offset_eq::match_x_minus_y(expr* e, expr*& x, expr*& y) const {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 4c67d187c2c..b4611b72e16 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -745,6 +745,7 @@ bool theory_seq::is_solved() {
 */
 void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
     context & ctx = get_context();    
+    (void)ctx;
     DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); );
     svector<assumption> assumptions;
     const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
@@ -1885,6 +1886,7 @@ class theory_seq::seq_value_proc : public model_value_proc {
     svector<source_t>               m_source;
 public:
     seq_value_proc(theory_seq& th, enode* n, sort* s): th(th), m_node(n), m_sort(s) {
+        (void)m_node;
     }
     ~seq_value_proc() override {}
     void add_unit(enode* n) { 
@@ -3458,7 +3460,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
 
 void theory_seq::propagate_length_limit(expr* e) {
     unsigned k = 0;
-    expr* s = nullptr, *i = nullptr;
+    expr* s = nullptr;
     VERIFY(m_sk.is_length_limit(e, k, s));
     if (m_util.str.is_stoi(s)) {
         m_ax.add_stoi_axiom(s, k);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 15b1f988bc7..ede35db7b59 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -446,7 +446,7 @@ namespace smt {
         theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), new_ctx->get_fparams()); }
         char const * get_name() const override { return "seq"; }
         bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); }
-        bool is_safe_to_copy(bool_var v) const;
+        bool is_safe_to_copy(bool_var v) const override;
         theory_var mk_var(enode* n) override;
         void apply_sort_cnstr(enode* n, sort* s) override;
         void display(std::ostream & out) const override;
diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index 47a530bd8df..b06475a8d84 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -371,7 +371,6 @@ expr * ufbv_rewriter::rewrite(expr * n) {
             if (rewrite_visit_children(a)) {
                 func_decl * f = a->get_decl();
                 m_new_args.reset();
-                unsigned num_args = a->get_num_args();
                 bool all_untouched = true;
                 for (expr* o_child : *a) {
                     expr * n_child;