diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b522fe940..2ead2e4b2 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -393,7 +393,7 @@ void seq_rewriter::updt_params(params_ref const & p) {
     m_coalesce_chars = sp.coalesce_chars();
 }
 
-static void get_param_descrs(param_descrs & r) {
+void seq_rewriter::get_param_descrs(param_descrs & r) {
     seq_rewriter_params::collect_param_descrs(r);
 }
 
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index fb98701aa..9f73a9f9b 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1115,7 +1115,6 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
     (*rep)(result);
 
     // adjust result according to model converter.
-    unsigned arity = m_head->get_arity();
     model_ref md = alloc(model, m);
     md->register_decl(m_head, result);    
     model_converter_ref mc = ctx.get_model_converter();
diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
index 9c823c57d..dacb32d1b 100644
--- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp
@@ -74,7 +74,6 @@ namespace datalog {
                 bool_vector const& is_bound  = m_bound[i];
                 func_interp* f = old_model->get_func_interp(p);
                 expr_ref body(m);
-                unsigned arity_q = q->get_arity();
                 SASSERT(0 < p->get_arity());
 
                 if (f) {
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index dd90a2127..e575d766f 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -33,8 +33,8 @@ namespace smt {
           m(m),
           m_plugin(*reinterpret_cast<recfun::decl::plugin*>(m.get_plugin(get_family_id()))),
           m_util(m_plugin.u()), 
-          m_preds(m),
           m_disabled_guards(m),
+          m_preds(m),
           m_enabled_guards(m),
           m_num_rounds(0),
           m_q_case_expand(), 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3853e5f1f..21497fd6e 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4442,7 +4442,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
 
 app* theory_seq::mk_value(app* e) {
     expr_ref result(m);
-    expr* e0 = e;
     e = get_ite_value(e);
     result = m_rep.find(e);
 
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index acbfd1008..109439975 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -507,6 +507,7 @@ namespace smt {
         while (consistent && can_propagate()) {
             unsigned idx = m_asserted_atoms[m_asserted_qhead];
             m_asserted_qhead++;
+            std::cout << "propagate atom " << idx << "\n";
             consistent = propagate_atom(m_atoms[idx]);            
         }
     }
@@ -656,7 +657,9 @@ namespace smt {
             SASSERT(v2 != null_theory_var);
             SASSERT(pos2 || terms[1].second.is_minus_one());
         }            
-        TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";);
+        TRACE("utvpi", tout << (pos1?"$":"-$") << v1;
+              if (terms.size() == 2) tout << (pos2?" + $":" - $") << v2;
+              tout << " + " << weight << " <= 0\n";);
         edge_id id = m_graph.get_num_edges();
         th_var w1 = to_var(v1), w2 = to_var(v2);