diff --git a/src/muz_qe/hnf.cpp b/src/muz_qe/hnf.cpp
index bcc3501de..75a85061c 100644
--- a/src/muz_qe/hnf.cpp
+++ b/src/muz_qe/hnf.cpp
@@ -201,6 +201,7 @@ private:
             if (!m_sorts.empty()) {
                 proof* p1 = m.mk_pull_quant(fml, to_quantifier(fml1));
                 premise = mk_modus_ponens(premise, p1);
+                fml = fml1;
             }
         }
         head = fml0;
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 20448dc74..390803957 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -558,7 +558,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
                    lits.size(), lits.c_ptr(), 
                    params.size(), params.c_ptr());
     }
-    clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
+    ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
     if (dump_lemmas()) {
         char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA";
         ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
diff --git a/src/smt/theory_horn_ineq.h b/src/smt/theory_horn_ineq.h
index fac6e96df..ed96f25f6 100644
--- a/src/smt/theory_horn_ineq.h
+++ b/src/smt/theory_horn_ineq.h
@@ -91,7 +91,6 @@ namespace smt {
         typedef svector<th_var> th_var_vector;
         typedef unsigned clause_id;
         typedef vector<std::pair<th_var, rational> >  coeffs;
-        static const clause_id null_clause_id = UINT_MAX;
 
         class clause;
         class graph;
@@ -108,7 +107,7 @@ namespace smt {
             atom(bool_var bv, int pos, int neg) : 
                 m_bvar(bv), m_true(false),
                 m_pos(pos), m_neg(neg) {}
-            virtual ~atom() {}
+            ~atom() {}
             bool_var get_bool_var() const { return m_bvar; }
             bool is_true() const { return m_true; }
             void assign_eh(bool is_true) { m_true = is_true; }
diff --git a/src/smt/theory_horn_ineq_def.h b/src/smt/theory_horn_ineq_def.h
index 505815b4f..f4fa7e8d7 100644
--- a/src/smt/theory_horn_ineq_def.h
+++ b/src/smt/theory_horn_ineq_def.h
@@ -27,6 +27,8 @@ Revision History:
 
 namespace smt {
 
+    static const unsigned null_clause_id = UINT_MAX;
+
     /**
        A clause represents an inequality of the form
        
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 8b19bdab8..9e8073ec2 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -78,7 +78,7 @@ namespace smt {
             atom(bool_var bv, int pos, int neg) : 
                 m_bvar(bv), m_true(false),
                 m_pos(pos), m_neg(neg) {}
-            virtual ~atom() {}
+            ~atom() {}
             bool_var get_bool_var() const { return m_bvar; }
             void assign_eh(bool is_true) { m_true = is_true; }
             int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 905270a46..af372ea50 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -54,8 +54,8 @@ namespace smt {
             m_arith_eq_adapter(*this, m_params, a),
             m_zero_int(null_theory_var),
             m_zero_real(null_theory_var),
-            m_asserted_qhead(0),
             m_nc_functor(*this),
+            m_asserted_qhead(0),
             m_agility(0.5),
             m_lia(false),
             m_lra(false),