diff --git a/src/ast/ast_pp_dot.cpp b/src/ast/ast_pp_dot.cpp
index df3de730f..e3782cb21 100644
--- a/src/ast/ast_pp_dot.cpp
+++ b/src/ast/ast_pp_dot.cpp
@@ -41,8 +41,8 @@ struct ast_pp_dot_st {
         m_pp(pp),
         m_next_id(0),
         m_id_map(),
-        m_to_print(),
         m_printed(),
+        m_to_print(),
         m_first(true) {}
 
     ~ast_pp_dot_st() = default;
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 13a7599a9..220295dad 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3076,8 +3076,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     split_fp(x, sgn, e, s);
     mk_is_nan(x, x_is_nan);
 
-    sort * fp_srt = m.get_sort(x);
-
     expr_ref unspec(m);
     mk_to_ieee_bv_unspecified(f, num, args, unspec);
 
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 31190a97f..83042cd6d 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -149,8 +149,6 @@ namespace spacer {
         expr_ref val(m), tmp(m);
         proof_ref pr(m);
         pr = m.mk_asserted(m.mk_true());
-        obj_map<expr, unsigned>::iterator it  = diseqs.begin();
-        obj_map<expr, unsigned>::iterator end = diseqs.end();
         for (auto const& kv : diseqs) {
             if (kv.m_value >= threshold) {
                 model.eval(kv.m_key, val);
diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp
index 244a97d22..87a21336c 100644
--- a/src/muz/spacer/spacer_virtual_solver.cpp
+++ b/src/muz/spacer/spacer_virtual_solver.cpp
@@ -81,6 +81,8 @@ static bool matches_fact(expr_ref_vector &args, expr* &match)
 }
 
 
+// TBD: move to ast/proofs/elim_aux_assertions
+
 class elim_aux_assertions {
     app_ref m_aux;
 public:
@@ -404,6 +406,7 @@ void virtual_solver::refresh()
     m_head = 0;
 }
 
+#ifdef NOT_USED_ANYWHERE
 void virtual_solver::reset()
 {
     SASSERT(!m_pushed);
@@ -411,6 +414,7 @@ void virtual_solver::reset()
     m_assertions.reset();
     m_factory.refresh();
 }
+#endif
 
 void virtual_solver::get_labels(svector<symbol> &r)
 {
diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h
index 14e05302e..3ccd89ef5 100644
--- a/src/muz/spacer/spacer_virtual_solver.h
+++ b/src/muz/spacer/spacer_virtual_solver.h
@@ -91,8 +91,9 @@ public:
     virtual void set_produce_models(bool f);
     virtual bool get_produce_models();
     virtual smt_params &fparams();
+#ifdef NOT_USED_ANYWHERE
     virtual void reset();
-
+#endif
     virtual void set_progress_callback(progress_callback *callback)
     {UNREACHABLE();}
 
diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp
index 2aaf2833f..472053fdc 100644
--- a/src/smt/theory_array_base.cpp
+++ b/src/smt/theory_array_base.cpp
@@ -218,7 +218,6 @@ namespace smt {
             ast_manager & m = get_manager();
             ext_skolems = alloc(func_decl_ref_vector, m);
             for (unsigned i = 0; i < dimension; ++i) {
-                sort * ext_sk_domain[2] = { s_array, s_array };
                 func_decl * ext_sk_decl = util.mk_array_ext(s_array, i);
                 ext_skolems->push_back(ext_sk_decl);
             }
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index ee94c5e57..2099eebf0 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -441,7 +441,7 @@ ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
 }
 
 
-// ----------------------
+// ---------------------
 // expr_substitution_simplifier
 
 bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) {
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 6cd94a3c1..56eea8d9a 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -95,7 +95,6 @@ class dom_simplify_tactic : public tactic {
     expr_ref_vector      m_trail, m_args;
     obj_map<expr, expr*> m_result;
     expr_dominators      m_dominators;
-    unsigned             m_scope_level;
     unsigned             m_depth;
     unsigned             m_max_depth;
     ptr_vector<expr>     m_empty;
@@ -128,8 +127,7 @@ public:
     dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
         m(m), m_simplifier(s), m_params(p), 
         m_trail(m), m_args(m), 
-        m_dominators(m), 
-        m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
+        m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
 
 
     virtual ~dom_simplify_tactic();