diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9bb2141a2..388218639 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -99,7 +99,7 @@ set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git")
 if (EXISTS "${GIT_DIR}")
   # Try to make CMake configure depend on the current git HEAD so that
   # a re-configure is triggered when the HEAD changes.
-  add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
+  add_git_dir_dependency("${CMAKE_SOURCE_DIR}" ADD_GIT_DEP_SUCCESS)
   if (ADD_GIT_DEP_SUCCESS)
     if (INCLUDE_GIT_HASH)
       get_git_head_hash("${GIT_DIR}" Z3GITHASH)
diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c
index 5696f5b89..50550106e 100644
--- a/examples/maxsat/maxsat.c
+++ b/examples/maxsat/maxsat.c
@@ -138,7 +138,7 @@ void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z
 
 /**
    \brief Assert soft constraints stored in the given array.
-   This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
+   This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
    It will also return an array containing these fresh variables.
 */
 Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) 
@@ -565,7 +565,7 @@ int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_as
 
 /**
   \brief Finds the maximal number of assumptions that can be satisfied.
-  An assumption is any formula preceeded with the :assumption keyword.
+  An assumption is any formula preceded with the :assumption keyword.
   "Hard" constraints can be supported by using the :formula keyword.
   
   Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.
diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index 8c18df7b2..9130d628c 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -220,7 +220,7 @@ lbool lackr::lazy() {
     lackr_model_constructor mc(m_m, m_info);
     push_abstraction();
     unsigned ackr_head = 0;
-    while (1) {
+    while (true) {
         m_st.m_it++;
         checkpoint();
         TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index cdc592527..604267536 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -913,7 +913,7 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (sgn == nullptr) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "sign cannot be a nullpointer");
-            return 0;
+            return false;
         }
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@@ -922,13 +922,13 @@ extern "C" {
         expr * e = to_expr(t);
         if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
-            return 0;
+            return false;
         }
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);
         if (!r || mpfm.is_nan(val)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
-            return 0;
+            return false;
         }
         *sgn = mpfm.sgn(val);
         return r;
@@ -1043,7 +1043,7 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (n == nullptr) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid nullptr argument");
-            return 0;
+            return false;
         }
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@@ -1055,7 +1055,7 @@ extern "C" {
         if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(e, val);
@@ -1065,10 +1065,10 @@ extern "C" {
             !mpzm.is_uint64(z)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         *n = mpzm.get_uint64(z);
-        return 1;
+        return true;
         Z3_CATCH_RETURN(0);
     }
 
@@ -1121,7 +1121,7 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (n == nullptr) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid null argument");
-            return 0;
+            return false;
         }
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@@ -1132,14 +1132,14 @@ extern "C" {
         if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(e, val);
         if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
             *n = 0;
-            return 0;
+            return false;
         }
         unsigned ebits = val.get().get_ebits();
         if (biased) {
@@ -1153,7 +1153,7 @@ extern "C" {
                   mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
                  mpfm.exp(val);
         }
-        return 1;
+        return true;
         Z3_CATCH_RETURN(0);
     }
 
@@ -1240,7 +1240,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_nan(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1254,7 +1254,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_inf(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1268,7 +1268,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_zero(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1282,7 +1282,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_normal(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1296,7 +1296,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_subnormal(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1310,7 +1310,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_positive(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
@@ -1324,7 +1324,7 @@ extern "C" {
         fpa_util & fu = ctx->fpautil();
         if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
-            return 0;
+            return false;
         }
         return fu.is_negative(to_expr(t));
         Z3_CATCH_RETURN(Z3_FALSE);
diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp
index 49aa09727..fe9faa2a5 100644
--- a/src/api/api_quant.cpp
+++ b/src/api/api_quant.cpp
@@ -132,7 +132,7 @@ extern "C" {
                                unsigned num_decls, Z3_sort const types[],
                                Z3_symbol const decl_names[],
                                Z3_ast body) {
-        return Z3_mk_quantifier(c, 1, weight, num_patterns, patterns, num_decls, types, decl_names, body);
+        return Z3_mk_quantifier(c, true, weight, num_patterns, patterns, num_decls, types, decl_names, body);
     }
 
     Z3_ast Z3_API Z3_mk_exists(Z3_context c,
@@ -141,7 +141,7 @@ extern "C" {
                                unsigned num_decls, Z3_sort const types[],
                                Z3_symbol const decl_names[],
                                Z3_ast body) {
-        return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, body);
+        return Z3_mk_quantifier(c, false, weight, num_patterns, patterns, num_decls, types, decl_names, body);
     }
 
     Z3_ast Z3_API Z3_mk_lambda(Z3_context c,
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 1b1820909..33af3ddde 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -277,7 +277,7 @@ namespace z3 {
          */
         sort fpa_rounding_mode();
         /**
-           \breif Sets RoundingMode of FloatingPoints.
+           \brief Sets RoundingMode of FloatingPoints.
          */
         void set_rounding_mode(rounding_mode rm);
         /**
@@ -291,7 +291,7 @@ namespace z3 {
            \brief Return a tuple constructor.
            \c name is the name of the returned constructor,
            \c n are the number of arguments, \c names and \c sorts are their projected sorts.
-           \c projs is an output paramter. It contains the set of projection functions.
+           \c projs is an output parameter. It contains the set of projection functions.
         */
         func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 703105356..d466d2e77 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8327,7 +8327,7 @@ def prove(claim, **keywords):
         print(s.model())
 
 def _solve_html(*args, **keywords):
-    """Version of funcion `solve` used in RiSE4Fun."""
+    """Version of function `solve` used in RiSE4Fun."""
     s = Solver()
     s.set(**keywords)
     s.add(*args)
@@ -8349,7 +8349,7 @@ def _solve_html(*args, **keywords):
         print(s.model())
 
 def _solve_using_html(s, *args, **keywords):
-    """Version of funcion `solve_using` used in RiSE4Fun."""
+    """Version of function `solve_using` used in RiSE4Fun."""
     if __debug__:
         _z3_assert(isinstance(s, Solver), "Solver object expected")
     s.set(**keywords)
@@ -8372,7 +8372,7 @@ def _solve_using_html(s, *args, **keywords):
         print(s.model())
 
 def _prove_html(claim, **keywords):
-    """Version of funcion `prove` used in RiSE4Fun."""
+    """Version of function `prove` used in RiSE4Fun."""
     if __debug__:
         _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
     s = Solver()
diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h
index 8f9e2470c..f15d8ff9c 100644
--- a/src/api/z3_optimization.h
+++ b/src/api/z3_optimization.h
@@ -146,7 +146,7 @@ extern "C" {
     Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
 
     /**
-       \brief Retrieve the unsat core for the last #Z3_optimize_chec
+       \brief Retrieve the unsat core for the last #Z3_optimize_check
        The unsat core is a subset of the assumptions \c a.
 
        def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))       
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 284c4df93..9cb685ccc 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -231,7 +231,7 @@ namespace datatype {
                 }
                 return s;
             }
-            catch (invalid_datatype) {
+            catch (const invalid_datatype &) {
                 m_manager->raise_exception("invalid datatype");
                 return nullptr;
             }
diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp
index d46388801..311133e05 100644
--- a/src/ast/for_each_expr.cpp
+++ b/src/ast/for_each_expr.cpp
@@ -58,7 +58,7 @@ bool has_skolem_functions(expr * n) {
     try {
         for_each_expr(p, n);
     }
-    catch (has_skolem_functions_ns::found) {
+    catch (const has_skolem_functions_ns::found &) {
         return true;
     }
     return false;
diff --git a/src/ast/occurs.cpp b/src/ast/occurs.cpp
index c76e73748..9ddb2fa56 100644
--- a/src/ast/occurs.cpp
+++ b/src/ast/occurs.cpp
@@ -58,7 +58,7 @@ bool occurs(expr * n1, expr * n2) {
     try {
         quick_for_each_expr(p, n2);
     }
-    catch (occurs_namespace::found) {
+    catch (const occurs_namespace::found &) {
         return true;
     }
     return false;
@@ -69,7 +69,7 @@ bool occurs(func_decl * d, expr * n) {
     try {
         quick_for_each_expr(p, n);
     }
-    catch (occurs_namespace::found) {
+    catch (const occurs_namespace::found &) {
         return true;
     }
     return false;
diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp
index f337ca638..f30df7890 100644
--- a/src/ast/rewriter/bv_bounds.cpp
+++ b/src/ast/rewriter/bv_bounds.cpp
@@ -111,7 +111,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
     numeral val, val1;
     unsigned bv_sz1;
 
-    if (0) {
+    if (false) {
         if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) {
             return record(to_app(lhs), val, val, negated, nis);
         }
@@ -125,7 +125,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
         return record(to_app(lhs), numeral::zero(), val, negated, nis);
     }
 
-    if (1) {
+    if (true) {
         numeral rhs_val;
         unsigned rhs_sz;
         if (m_m.is_eq(e, lhs, rhs)
@@ -343,7 +343,7 @@ bool bv_bounds::add_constraint(expr* e) {
     numeral val, val1;
     unsigned bv_sz1;
 
-    if (0) {
+    if (false) {
         if (m_m.is_eq(e, lhs, rhs) && to_bound(lhs) && m_bv_util.is_numeral(rhs, val, bv_sz1)) {
             return add_bound_unsigned(to_app(lhs), val, val, negated);
         }
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 57e15c6a3..47c919d4a 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -476,7 +476,7 @@ struct check_logic::imp {
             quick_for_each_expr(*this, n);
             return true;
         }
-        catch (failed) {
+        catch (const failed &) {
             return false;
         }
     }
@@ -495,7 +495,7 @@ struct check_logic::imp {
             check_sort(f->get_range());
             return true;
         }
-        catch (failed) {
+        catch (const failed &) {
             return false;
         }
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8a23f80a0..7b7f81561 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1833,7 +1833,7 @@ void cmd_context::validate_model() {
                     for_each_expr(contains_underspecified, a);
                     for_each_expr(contains_underspecified, r);
                 }
-                catch (contains_underspecified_op_proc::found) {
+                catch (const contains_underspecified_op_proc::found &) {
                     continue;
                 }
                 TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0););
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index aa4fc5a39..528c10537 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -1989,7 +1989,7 @@ namespace algebraic_numbers {
                     TRACE("anum_eval_sign", tout << "all variables are assigned to rationals, value of p: " << r << "\n";);
                     return qm().sign(r);
                 }
-                catch (opt_var2basic::failed) {
+                catch (const opt_var2basic::failed &) {
                     // continue
                 }
 
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 24658fdcf..00a4d0593 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -4493,7 +4493,7 @@ namespace polynomial {
                         }
                         #endif
                     }
-                    catch (sparse_mgcd_failed) {
+                    catch (const sparse_mgcd_failed &) {
                         flet<bool> use_prs(m_use_prs_gcd, false);
                         gcd_prs(u, v, x, r);
                     }
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 935fd5e19..7a3f2e7b3 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -183,7 +183,7 @@ class subpaving_tactic : public tactic {
                     process_clause(g.form(i));
                 }
             }
-            catch (subpaving::exception) {
+            catch (const subpaving::exception &) {
                 throw tactic_exception("failed to internalize goal into subpaving module");
             }
         }
@@ -195,7 +195,7 @@ class subpaving_tactic : public tactic {
             try {
                 (*m_ctx)();
             }
-            catch (subpaving::exception) {
+            catch (const subpaving::exception &) {
                 throw tactic_exception("failed building subpaving tree...");
             }
             if (m_display) {
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 0dbeba5b3..fe1f101b1 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -422,7 +422,7 @@ namespace datalog {
         try {
             quick_for_each_expr(proc, fml);
         }
-        catch (contains_predicate_proc::found) {
+        catch (const contains_predicate_proc::found &) {
             return true;
         }
         return false;
diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp
index f0cbc0620..1e6196950 100644
--- a/src/muz/base/hnf.cpp
+++ b/src/muz/base/hnf.cpp
@@ -219,7 +219,7 @@ private:
             quick_for_each_expr(m_proc, m_mark1, fml);
             m_mark1.reset();
         }
-        catch (contains_predicate_proc::found) {
+        catch (const contains_predicate_proc::found &) {
             m_mark1.reset();
             return true;
         }
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 30b68ebf6..9a9043f2f 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2737,7 +2737,7 @@ lbool context::solve(unsigned from_lvl)
             // }
         }
         VERIFY (validate ());
-    } catch (unknown_exception)
+    } catch (const unknown_exception &)
     {}
 
     if (m_last_result == l_true) {
diff --git a/src/muz/spacer/spacer_farkas_learner.cpp b/src/muz/spacer/spacer_farkas_learner.cpp
index d97bee49f..291226b55 100644
--- a/src/muz/spacer/spacer_farkas_learner.cpp
+++ b/src/muz/spacer/spacer_farkas_learner.cpp
@@ -95,7 +95,7 @@ bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e, ast_manag
     is_pure_expr_proc proc(symbs, m);
     try {
         for_each_expr(proc, e);
-    } catch (is_pure_expr_proc::non_pure) {
+    } catch (const is_pure_expr_proc::non_pure &) {
         return false;
     }
     return true;
diff --git a/src/muz/spacer/spacer_iuc_proof.cpp b/src/muz/spacer/spacer_iuc_proof.cpp
index b6a522b76..949507fb4 100644
--- a/src/muz/spacer/spacer_iuc_proof.cpp
+++ b/src/muz/spacer/spacer_iuc_proof.cpp
@@ -88,7 +88,7 @@ bool iuc_proof::is_core_pure(expr* e) const
     try {
         for_each_expr(proc, e);
     }
-    catch (is_pure_expr_proc::non_pure)
+    catch (const is_pure_expr_proc::non_pure &)
     {return false;}
 
     return true;
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index 856207463..817d620c9 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -247,7 +247,7 @@ bool has_zk_const(expr *e){
     try {
         for_each_expr(p, e);
     }
-    catch (has_zk_const_ns::found) {
+    catch (const has_zk_const_ns::found &) {
         return true;
     }
     return false;
diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp
index a11ab4d9e..f3307a596 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -120,7 +120,7 @@ struct index_lt_proc : public std::binary_function<app*, app *, bool> {
             for (expr *e : v)
                 quick_for_each_expr(fn, visited, e);
         }
-        catch (has_nlira_functor::found ) {
+        catch (const has_nlira_functor::found &) {
             return true;
         }
         return false;
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index ec01218f1..2a5f1e2cc 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -891,7 +891,7 @@ namespace {
             for_each_expr(cs, fml);
             return false;
         }
-        catch(found) {
+        catch(const found &) {
             return true;
         }
     }
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index c60c770bf..b5be996dc 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -415,7 +415,7 @@ namespace tb {
             try {
                 quick_for_each_expr(p, t);
             }
-            catch (non_constructor) {
+            catch (const non_constructor &) {
                 return false;
             }
             return true;
diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp
index 6a8f0ce81..626109528 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_array_instantiation.cpp
@@ -300,7 +300,7 @@ namespace datalog {
     expr_ref_vector res(m);
 
     svector<unsigned> chosen(arg_correspondance.size(), 0u);
-    while(1)
+    while(true)
     {
       expr_ref_vector new_args(m);
       for(unsigned i=0;i<chosen.size();i++)
diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp
index f0d9a8843..7e0356e7e 100644
--- a/src/muz/transforms/dl_mk_elim_term_ite.cpp
+++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp
@@ -57,7 +57,7 @@ namespace {
         term_ite_proc f(m);
         try {
             quick_for_each_expr(f, e);
-        } catch (term_ite_proc::found) {
+        } catch (const term_ite_proc::found &) {
             return true;
         }
         return false;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ff37bfa95..d9c3457fa 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -706,7 +706,7 @@ namespace opt {
                 quick_for_each_expr(proc, visited, f);
             }
         }
-        catch (is_bv::found) {
+        catch (const is_bv::found &) {
             return false;
         }
         return true;
@@ -737,7 +737,7 @@ namespace opt {
         try {
             quick_for_each_expr(proc, visited, p);
         }
-        catch (is_propositional_fn::found) {
+        catch (const is_propositional_fn::found &) {
             return false;
         }
         return true;
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 1a16b817b..58b16717d 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -3084,7 +3084,7 @@ namespace smt2 {
                                            << ": " << ex.msg() << "\")" << std::endl;
                     exit(ex.error_code());
                 }
-                catch (stop_parser_exception) {
+                catch (const stop_parser_exception &) {
                     m_scanner.stop_caching();
                     return !found_errors;
                 }
diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp
index c9d00ebcc..48c42c240 100644
--- a/src/parsers/util/simple_parser.cpp
+++ b/src/parsers/util/simple_parser.cpp
@@ -118,7 +118,7 @@ bool simple_parser::parse(std::istream & in, expr_ref & result) {
         if (!result)
             throw parser_error();
     }
-    catch (parser_error) {
+    catch (const parser_error &) {
         warning_msg("parser error");
         return false;
     } 
diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp
index 5499d638d..7ade47458 100644
--- a/src/qe/qe_datatypes.cpp
+++ b/src/qe/qe_datatypes.cpp
@@ -61,7 +61,7 @@ namespace qe {
                     project_nonrec(model, vars, lits);
                 }
             }
-            catch (cant_project) {
+            catch (const cant_project &) {
                 TRACE("qe", tout << "can't project:" << mk_pp(var, m) << "\n";);
                 return false;
             }
diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp
index faa9cfed8..97b044f5b 100644
--- a/src/qe/qe_term_graph.cpp
+++ b/src/qe/qe_term_graph.cpp
@@ -62,7 +62,7 @@ namespace qe {
             is_pure_ns::proc v(is_var);
             quick_for_each_expr(v, e);
         }
-        catch (is_pure_ns::found) {
+        catch (const is_pure_ns::found &) {
             return false;
         }
         return true;
diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp
index bd1745765..e7b0632d8 100644
--- a/src/sat/sat_bdd.cpp
+++ b/src/sat/sat_bdd.cpp
@@ -87,7 +87,7 @@ namespace sat {
             try {
                 return apply_rec(arg1, arg2, op);
             }
-            catch (mem_out) {
+            catch (const mem_out &) {
                 try_reorder();
                 if (!first) throw;
                 first = false;
@@ -546,7 +546,7 @@ namespace sat {
             try {
                 return bdd(mk_not_rec(b.root), this);
             }
-            catch (mem_out) {
+            catch (const mem_out &) {
                 try_reorder();
                 if (!first) throw;
                 first = false;
@@ -575,7 +575,7 @@ namespace sat {
             try {
                 return bdd(mk_ite_rec(c.root, t.root, e.root), this); 
             }
-            catch (mem_out) {
+            catch (const mem_out &) {
                 try_reorder();
                 if (!first) throw;
                 first = false;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index f48ac57a6..2032445ed 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1147,7 +1147,7 @@ namespace sat {
 
             }
         }
-        catch (abort_solver) {
+        catch (const abort_solver &) {
             m_reason_unknown = "sat.giveup";
             return l_undef;
         }
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 02b0e16be..58158ec06 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -261,7 +261,7 @@ namespace smt {
         try {
             for_each_expr(*this, m_visited, n);
         }
-        catch (is_model_value) {
+        catch (const is_model_value &) {
             return true;
         }
         return false;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index b8b22b067..30ea7b18e 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -177,7 +177,7 @@ namespace smt {
                 try {
                     for_each_expr(*this, m_visited, n);
                 }
-                catch (is_model_value) {
+                catch (const is_model_value &) {
                     return true;
                 }
                 return false;
@@ -2892,7 +2892,7 @@ namespace smt {
                 try {
                     for_each_expr(oc, m_visited, def);
                 }
-                catch (occurs) {
+                catch (const occurs &) {
                     return false;
                 }
                 return true;
@@ -2981,7 +2981,7 @@ namespace smt {
                     try {
                         process(f);
                     }
-                    catch (found_satisfied_subset) {
+                    catch (const found_satisfied_subset &) {
                         set_interp();
                         copy_non_satisfied(qcandidates, new_qs);
                         return true;
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index a2c6c1191..70ce6b397 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -156,9 +156,9 @@ namespace smt {
             row_entry & operator[](unsigned idx) { return m_entries[idx]; }
             row_entry const & operator[](unsigned idx) const { return m_entries[idx]; }
             typename vector<row_entry>::iterator begin_entries() { return m_entries.begin(); }
-            const typename vector<row_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
+            typename vector<row_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
             typename vector<row_entry>::iterator end_entries() { return m_entries.end(); }
-            const typename vector<row_entry>::const_iterator end_entries() const { return m_entries.end(); }
+            typename vector<row_entry>::const_iterator end_entries() const { return m_entries.end(); }
             row_entry & add_row_entry(int & pos_idx);
             void del_row_entry(unsigned idx);
             void compress(vector<column> & cols); 
@@ -195,9 +195,9 @@ namespace smt {
             col_entry & operator[](unsigned idx) { return m_entries[idx]; }
             col_entry const & operator[](unsigned idx) const { return m_entries[idx]; }
             typename svector<col_entry>::iterator begin_entries() { return m_entries.begin(); }
-            const typename svector<col_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
+            typename svector<col_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
             typename svector<col_entry>::iterator end_entries() { return m_entries.end(); }
-            const typename svector<col_entry>::const_iterator end_entries() const { return m_entries.end(); }
+            typename svector<col_entry>::const_iterator end_entries() const { return m_entries.end(); }
             col_entry & add_col_entry(int & pos_idx);
             void del_col_entry(unsigned idx);
         };
diff --git a/src/smt/uses_theory.cpp b/src/smt/uses_theory.cpp
index 517951a7b..64565dc78 100644
--- a/src/smt/uses_theory.cpp
+++ b/src/smt/uses_theory.cpp
@@ -41,7 +41,7 @@ bool uses_theory(expr * n, family_id fid, expr_mark & visited) {
     try {
         for_each_expr(p, visited, n);
     }
-    catch (uses_theory_ns::found) {
+    catch (const uses_theory_ns::found &) {
         return true;
     }
     return false;
diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp
index 5839ff7a2..67fca873e 100644
--- a/src/tactic/arith/bv2real_rewriter.cpp
+++ b/src/tactic/arith/bv2real_rewriter.cpp
@@ -89,7 +89,7 @@ bool bv2real_util::contains_bv2real(expr* e) const {
     try {
         for_each_expr(p, e);
     }
-    catch (contains_bv2real_proc::found) {
+    catch (const contains_bv2real_proc::found &) {
         return true;
     }
     return false;
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index 669ded49d..d198ce498 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -226,7 +226,7 @@ class fix_dl_var_tactic : public tactic {
                 }
                 return most_occs();
             }
-            catch (failed) {
+            catch (const failed &) {
                 return nullptr;
             }
         }
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index db1c22866..c177f35be 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -156,7 +156,7 @@ class lia2pb_tactic : public tactic {
                 }
                 return true;
             }
-            catch (failed) {
+            catch (const failed &) {
                 return false;
             }
         }
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index f36e3a6db..7a64c9f16 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -1034,7 +1034,7 @@ struct is_pb_probe : public probe {
             
             return true;
         }
-        catch (pb2bv_tactic::non_pb) {
+        catch (const pb2bv_tactic::non_pb &) {
             return false;
         }
     }
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index b81bc5687..bf9ca4101 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -371,7 +371,7 @@ class bv1_blaster_tactic : public tactic {
                     for_each_expr_core<visitor, expr_fast_mark1, false, true>(proc, visited, f);
                 }
             }
-            catch (not_target) {
+            catch (const not_target &) {
                 return false;
             }
             return true;
diff --git a/src/tactic/goal.h b/src/tactic/goal.h
index 4125fab99..fa2f16eb6 100644
--- a/src/tactic/goal.h
+++ b/src/tactic/goal.h
@@ -195,7 +195,7 @@ bool test(goal const & g, Predicate & proc) {
         for (unsigned i = 0; i < sz; i++)
             quick_for_each_expr(proc, visited, g.form(i));
     }
-    catch (typename Predicate::found) {
+    catch (const typename Predicate::found &) {
         return true;
     }
     return false;
diff --git a/src/tactic/probe.cpp b/src/tactic/probe.cpp
index dcd1dc500..432c9d123 100644
--- a/src/tactic/probe.cpp
+++ b/src/tactic/probe.cpp
@@ -524,7 +524,7 @@ public:
             }
             return false;
         }
-        catch (found) {
+        catch (const found &) {
             return true;
         }
     }
@@ -554,7 +554,7 @@ public:
             }
             return false;
         }
-        catch (found) {
+        catch (const found &) {
             return true;
         }
     }
diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp
index ee8a4605b..66a26be00 100644
--- a/src/tactic/ufbv/ufbv_rewriter.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter.cpp
@@ -870,7 +870,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) {
                 m_cache.insert(p);
                 continue;
             }
-            catch (match_args_aux_proc::no_match) {
+            catch (const match_args_aux_proc::no_match &) {
                 return false;
             }
         }
diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h
index bb6cdefc8..1a0ee1bdc 100644
--- a/src/util/lp/static_matrix.h
+++ b/src/util/lp/static_matrix.h
@@ -93,7 +93,7 @@ public:
         unsigned        m_row;
     public:
         ref_row(const static_matrix & m, unsigned row): m_matrix(m), m_row(row) {}
-        const T operator[](unsigned col) const { return m_matrix.get_elem(m_row, col); }
+        T operator[](unsigned col) const { return m_matrix.get_elem(m_row, col); }
     };
 
 public: