diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index f27c9ffcf..d65960857 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -431,7 +431,8 @@ struct poly_rewriter<Config>::hoist_cmul_lt {
     hoist_cmul_lt(poly_rewriter<Config> & r):m_r(r) {}
 
     bool operator()(expr * t1, expr * t2) const {
-        expr * pp1, * pp2;
+        expr * pp1 = nullptr;
+        expr * pp2 = nullptr;
         numeral c1, c2;
         bool is_mul1 = m_r.is_mul(t1, c1, pp1);
         bool is_mul2 = m_r.is_mul(t2, c2, pp2);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index dfb6542d6..4d4c4f708 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -336,9 +336,9 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
             UNREACHABLE();
         }
         // TODO: add rewrite rules support
-        expr * def;
-        proof * def_pr;
-        quantifier * def_q;
+        expr * def = nullptr;
+        proof * def_pr = nullptr;
+        quantifier * def_q = nullptr;
         // When get_macro succeeds, then
         // we know that:
         // forall X. f(X) = def[X]
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 4e8806d62..56a354ee8 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -395,7 +395,7 @@ class set_option_cmd : public set_get_option_cmd {
             env_params::updt_params();
             ctx.global_params_updated();
         }
-        catch (gparams::exception ex) {
+        catch (const gparams::exception & ex) {
             throw cmd_exception(ex.msg());
         }
     }
@@ -620,7 +620,7 @@ public:
             try {
                 ctx.regular_stream() << gparams::get_value(opt) << std::endl;
             }
-            catch (gparams::exception ex) {
+            catch (const gparams::exception & ex) {
                 ctx.print_unsupported(opt, m_line, m_pos);
             }
         }
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 43e7bdff8..773f328ab 100644
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -281,7 +281,7 @@ bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof, std::vector<ast> &v
         _proof = cook(proof);
     }
     else if(vars.size()) {
-        model_ref(_m);
+        model_ref _m;
         s.get_model(_m);
         if (!_m.get()) {
             SASSERT(l_undef == res);
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index 8c2016149..9efb1a383 100644
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -912,7 +912,7 @@ public:
                 if(!add_local_antes(arg, hyps, dk == PR_UNIT_RESOLUTION && i == 0))
                     return false;
             }
-            catch (non_lit_local_ante) {
+            catch (const non_lit_local_ante &) {
                 std::cout << "\n";
                 show_step(proof);
                 show(conc(proof));
@@ -1138,7 +1138,7 @@ public:
             try {
                 res = iproof->make_resolution(pnode,neg,pos);
             }
-            catch (const iz3proof::proof_error){
+            catch (const iz3proof::proof_error &){
                 std::cout << "\nresolution error in theory lemma\n";
                 std::cout << "lits:\n";
                 for(unsigned j = 0; j < lits.size(); j++)
@@ -1212,7 +1212,7 @@ public:
             try {
                 res = iproof->make_resolution(pnode,neg,pos);
             }
-            catch (const iz3proof::proof_error){
+            catch (const iz3proof::proof_error &){
                 std::cout << "\nresolution error in theory lemma\n";
                 std::cout << "lits:\n";
                 for(unsigned j = 0; j < lits.size(); j++)
@@ -1418,7 +1418,7 @@ public:
             try {
                 return iproof->make_resolution(pnode,neg,pos);
             }
-            catch (const iz3proof::proof_error){
+            catch (const iz3proof::proof_error &){
                 std::cout << "resolution error in unit_resolution, position" << position << "\n";
                 show_step(proof);
                 throw invalid_lemma();
diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp
index 16a9a9a9e..c43b74f0d 100644
--- a/src/math/subpaving/subpaving.cpp
+++ b/src/math/subpaving/subpaving.cpp
@@ -121,7 +121,7 @@ namespace subpaving {
                 int2mpf(c, m_c);
                 return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
             }
-            catch (f2n<mpf_manager>::exception) {
+            catch (const f2n<mpf_manager>::exception &) {
                 throw subpaving::exception();
             }
         }
@@ -135,7 +135,7 @@ namespace subpaving {
                 m.set(m_c, k);
                 return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open));
             }
-            catch (f2n<mpf_manager>::exception) {
+            catch (const f2n<mpf_manager>::exception &) {
                 throw subpaving::exception();
             }
         }
@@ -178,7 +178,7 @@ namespace subpaving {
                 int2hwf(c, m_c);
                 return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
             }
-            catch (f2n<mpf_manager>::exception) {
+            catch (const f2n<mpf_manager>::exception &) {
                 throw subpaving::exception();
             }
         }
@@ -192,7 +192,7 @@ namespace subpaving {
                 m.set(m_c, k);
                 return reinterpret_cast<ineq*>(m_ctx.mk_ineq(x, m_c, lower, open));
             }
-            catch (f2n<mpf_manager>::exception) {
+            catch (const f2n<mpf_manager>::exception &) {
                 throw subpaving::exception();
             }
         }
@@ -236,7 +236,7 @@ namespace subpaving {
                 int2fpoint(c, m_c);
                 return this->m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs);
             }
-            catch (typename context_fpoint::numeral_manager::exception) {
+            catch (const typename context_fpoint::numeral_manager::exception &) {
                 throw subpaving::exception();
             }
         }
@@ -251,7 +251,7 @@ namespace subpaving {
                 m.set(m_c, m_qm, k);
                 return reinterpret_cast<ineq*>(this->m_ctx.mk_ineq(x, m_c, lower, open));
             }
-            catch (typename context_fpoint::numeral_manager::exception) {
+            catch (const typename context_fpoint::numeral_manager::exception &) {
                 throw subpaving::exception();
             }
         }
diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index bb129fee7..cf93fbfad 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -1310,7 +1310,7 @@ bool context_t<C>::relevant_new_bound(var x, numeral const & k, bool lower, bool
         TRACE("subpaving_relevant_bound", tout << "new bound is relevant\n";);
         return true;
     }
-    catch (typename C::exception) {
+    catch (const typename C::exception &) {
         // arithmetic module failed.
         set_arith_failed();
         return false;
@@ -1722,7 +1722,7 @@ void context_t<C>::propagate(node * n, bound * b) {
                 }
             }
         }
-        catch (typename C::exception) {
+        catch (const typename C::exception &) {
             // arithmetic module failed, ignore constraint
             set_arith_failed();
         }
diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp
index 9cc13b897..6596cc3b7 100644
--- a/src/shell/datalog_frontend.cpp
+++ b/src/shell/datalog_frontend.cpp
@@ -246,7 +246,7 @@ unsigned read_datalog(char const * file) {
             false);
 
     }
-    catch (out_of_memory_error) {
+    catch (const out_of_memory_error &) {
         std::cout << "\n\nOUT OF MEMORY!\n\n";        
         display_statistics(
             std::cout,
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 5040f1034..944efe6ce 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -31,6 +31,7 @@ Revision History:
 #include "smt/params/theory_arith_params.h"
 #include "smt/arith_eq_adapter.h"
 #include "smt/proto_model/numeral_factory.h"
+#include "smt/smt_context.h"
 #include "util/obj_pair_hashtable.h"
 #include "smt/old_interval.h"
 #include "math/grobner/grobner.h"
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 126594b06..dde75c4bc 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1423,9 +1423,9 @@ namespace smt {
         //     len(hd) = i
         //     str.indexof(tl, N, 0)
 
-        expr * H; // "haystack"
-        expr * N; // "needle"
-        expr * i; // start index
+        expr * H = nullptr; // "haystack"
+        expr * N = nullptr; // "needle"
+        expr * i = nullptr; // start index
         u.str.is_index(e, H, N, i);
 
         expr_ref minus_one(m_autil.mk_numeral(rational::minus_one(), true), m);
@@ -6768,7 +6768,7 @@ namespace smt {
         expr * sub2;
         if (u.re.is_to_re(re, sub1)) {
             SASSERT(u.str.is_string(sub1));
-            zstring(str);
+            zstring str;
             u.str.is_string(sub1, str);
             lens.insert(str.length());
         } else if (u.re.is_concat(re, sub1, sub2)) {
@@ -6951,8 +6951,8 @@ namespace smt {
         ast_manager & m = get_manager();
 
         expr_ref_vector rhs(m);
-        expr * str;
-        expr * re;
+        expr * str = nullptr;
+        expr * re = nullptr;
         u.str.is_in_re(str_in_re, str, re);
         expr_ref strlen(mk_strlen(str), m);
 
@@ -9929,8 +9929,8 @@ namespace smt {
             bool regex_axiom_add = false;
             for (obj_hashtable<expr>::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) {
                 expr * str_in_re = *it;
-                expr * str;
-                expr * re;
+                expr * str = nullptr;
+                expr * re = nullptr;
                 u.str.is_in_re(str_in_re, str, re);
                 lbool current_assignment = ctx.get_assignment(str_in_re);
                 TRACE("str", tout << "regex term: " << mk_pp(str, m) << " in " << mk_pp(re, m) << " : " << current_assignment << std::endl;);
@@ -9944,7 +9944,7 @@ namespace smt {
 
                         if (regex_term_to_length_constraint.contains(str_in_re)) {
                             // use existing length constraint
-                            expr * top_level_length_constraint;
+                            expr * top_level_length_constraint = nullptr;
                             regex_term_to_length_constraint.find(str_in_re, top_level_length_constraint);
 
                             ptr_vector<expr> extra_length_vars;
@@ -10473,8 +10473,8 @@ namespace smt {
                 // that's consistent with the current length information
                 for (ptr_vector<expr>::iterator term_it = str_in_re_terms.begin();
                         term_it != str_in_re_terms.end(); ++term_it) {
-                    expr * _unused;
-                    expr * re;
+                    expr * _unused = nullptr;
+                    expr * re = nullptr;
                     SASSERT(u.str.is_in_re(*term_it));
                     u.str.is_in_re(*term_it, _unused, re);
 
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index 6afac32b8..f6e12275f 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -1522,7 +1522,7 @@ public:
             }
             SASSERT(ref_count(r) >= 1);
         }
-    catch (aig_exception ex) {
+    catch (const aig_exception & ex) {
         dec_ref(r);
         throw ex;
     }
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 9253b7172..c95a79ff7 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -263,8 +263,8 @@ class solve_eqs_tactic : public tactic {
         bool solve_arith_core(app * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
             SASSERT(m_a_util.is_add(lhs));
             bool is_int  = m_a_util.is_int(lhs);
-            expr * a; 
-            expr * v;
+            expr * a = nullptr; 
+            expr * v = nullptr;
             rational a_val;
             unsigned num = lhs->get_num_args();
             unsigned i;
diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp
index dd934831c..c78489f21 100644
--- a/src/test/mpff.cpp
+++ b/src/test/mpff.cpp
@@ -35,7 +35,7 @@ static void tst1() {
             std::cout << i << ": " << a << "\n";
         }
     }
-    catch (z3_exception & ex) {
+    catch (const z3_exception & ex) {
         std::cout << ex.msg() << "\n";
     }
 }
@@ -432,7 +432,7 @@ static void tst_limits(unsigned prec) {
     m.round_to_plus_inf();
     bool overflow = false;
     try { m.inc(a); }
-    catch (mpff_manager::overflow_exception) { overflow = true; }
+    catch (const mpff_manager::overflow_exception &) { overflow = true; }
     VERIFY(overflow);
     m.set_max(a);
     m.dec(a);
@@ -446,7 +446,7 @@ static void tst_limits(unsigned prec) {
     ENSURE(m.eq(a, b));
     overflow = true;
     try { m.dec(a); }
-    catch (mpff_manager::overflow_exception) { overflow = true; }
+    catch (const mpff_manager::overflow_exception &) { overflow = true; }
     ENSURE(overflow);
     m.round_to_plus_inf();
     m.set_min(a);
diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h
index 9d3a0e0aa..5c33db8c6 100644
--- a/src/util/lp/lar_constraints.h
+++ b/src/util/lp/lar_constraints.h
@@ -84,7 +84,6 @@ struct lar_term_constraint: public lar_base_constraint {
 class lar_constraint : public lar_base_constraint {
 public:
     vector<std::pair<mpq, var_index>> m_coeffs;
-    lar_constraint() {} 
     lar_constraint(const vector<std::pair<mpq, var_index>> & left_side, lconstraint_kind kind, const mpq & right_side)
         :  lar_base_constraint(kind, right_side), m_coeffs(left_side) {}