diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 22cbf21cc..de4156747 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -311,9 +311,10 @@ namespace opt {
                      mk_elim_uncnstr_tactic(m),
                      mk_simplify_tactic(m));   
         opt_params optp(m_params);
+        tactic_ref tac2, tac3;
         if (optp.elim_01()) {
-            tactic_ref tac2 = mk_elim01_tactic(m);
-            tactic_ref tac3 = mk_lia2card_tactic(m);
+            tac2 = mk_elim01_tactic(m);
+            tac3 = mk_lia2card_tactic(m);
             params_ref lia_p;
             lia_p.set_bool("compile_equality", optp.pb_compile_equality());
             tac3->updt_params(lia_p);
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index d63f0ae00..6df30ee3f 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -2435,7 +2435,7 @@ namespace qe {
     
     class simplify_solver_context : public i_solver_context {
         ast_manager&             m;
-        smt_params         m_fparams;
+        smt_params               m_fparams;
         app_ref_vector*          m_vars;
         expr_ref*                m_fml;
         ptr_vector<contains_app> m_contains;
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 7aa39b99a..aa0bff164 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -28,11 +28,6 @@ Notes:
 #include "sparse_matrix_def.h"
 #include "simplex_def.h"
 
-namespace simplex {
-template class simplex<mpq_ext>;
-template class sparse_matrix<mpq_ext>;
-};
-
 
 namespace smt {
 
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 41732f0a6..117e2133d 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -104,10 +104,10 @@ struct card2bv_rewriter_cfg : public default_rewriter_cfg {
 
 template class rewriter_tpl<card2bv_rewriter_cfg>;
 
-class pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
+class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
     card2bv_rewriter_cfg m_cfg;
 public:
-    pb_rewriter(ast_manager & m):
+    card_pb_rewriter(ast_manager & m):
         rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
         m_cfg(m) {}
 };
@@ -116,7 +116,7 @@ class card2bv_tactic : public tactic {
     ast_manager &              m;
     params_ref                 m_params;
     th_rewriter                m_rw1;
-    pb_rewriter                m_rw2;
+    card_pb_rewriter           m_rw2;
     
 public:
 
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 95db962a7..32f3fd7f7 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -31,6 +31,9 @@ struct simplify_tactic::imp {
         m_num_steps(0) {
     }
 
+    ~imp() {
+    }
+
     ast_manager & m() const { return m_manager; }
 
     void set_cancel(bool f) {