diff --git a/CMakeLists.txt b/CMakeLists.txt
index b109eb50b..a086afd71 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -218,12 +218,17 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
 ################################################################################
 # C++ language version
 ################################################################################
-# FIXME: Use CMake's own mechanism for selecting language version
-if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
-  z3_add_cxx_flag("-std=c++11" REQUIRED)
-else()
-  message(AUTHOR_WARNING "Not setting C++ language version for compiler")
-endif()
+if ("${CMAKE_VERSION}" VERSION_LESS "3.1")
+  # FIXME: Drop this when we upgrade to newer CMake versions.
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
+    z3_add_cxx_flag("-std=c++11" REQUIRED)
+  else()
+    message(AUTHOR_WARNING "Not setting C++ language version for compiler")
+  endif()
+else ()
+  set(CMAKE_CXX_STANDARD 11)
+  set(CMAKE_CXX_STANDARD_REQUIRED ON)
+endif ()
 
 ################################################################################
 # Platform detection
diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 86e7039dd..a99ec6b1e 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -1,5 +1,22 @@
 RELEASE NOTES
 
+Version 4.7.1
+=============
+
+- New requirements:
+  - uses stdbool and stdint as part of z3.h
+
+- New features:
+  - none
+
+- Removed features:
+  - none
+
+- Notes:
+   This is a minor release prior to a set of planned major updates.
+   It uses minor version 7 to indicate that the use of stdbool and
+   stdint are breaking changes to consumers of the C-based API.
+
 Version 4.6.0
 =============
 
diff --git a/examples/python/parallel.py b/examples/python/parallel.py
new file mode 100644
index 000000000..42ff50927
--- /dev/null
+++ b/examples/python/parallel.py
@@ -0,0 +1,36 @@
+from z3 import *
+from multiprocessing.pool import ThreadPool
+from copy import deepcopy
+
+pool = ThreadPool(8)
+x = Int('x')
+
+assert x.ctx == main_ctx()
+
+
+def calculate(x, n, ctx):
+    """ Do a simple computation with a context"""
+    assert x.ctx == ctx
+    assert x.ctx != main_ctx()
+
+    # Parallel creation of z3 object
+    condition = And(x < 2, x > n, ctx)
+
+    # Parallel solving
+    solver = Solver(ctx=ctx)
+    solver.add(condition)
+    solver.check()
+
+
+for i in range(100):
+    # Create new context for the computation
+    # Note that we need to do this sequentially, as parallel access to the current context or its objects
+    # will result in a segfault
+    i_context = Context()
+    x_i = deepcopy(x).translate(i_context)
+
+    # Kick off parallel computation
+    pool.apply_async(calculate, [x_i, i, i_context])
+
+pool.close()
+pool.join()
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 60470faa7..1391eee87 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1932,8 +1932,14 @@ class MLComponent(Component):
             OCAML_FLAGS = ''
             if DEBUG_MODE:
                 OCAML_FLAGS += '-g'
-            OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
-            OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
+
+            if OCAMLFIND:
+                # Load Big_int, which is no longer part of the standard library, via the num package: https://github.com/ocaml/num
+                OCAMLCF = OCAMLFIND + ' ' + 'ocamlc -package num' + ' ' + OCAML_FLAGS
+                OCAMLOPTF = OCAMLFIND + ' ' + 'ocamlopt -package num' + ' ' + OCAML_FLAGS
+            else:
+                OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
+                OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
 
             src_dir = self.to_src_dir
             mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index b4dab6926..8d7825335 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2385,6 +2385,7 @@ namespace z3 {
 
     class optimize : public object {
         Z3_optimize m_opt;
+        
     public:
         class handle {
             unsigned m_h;
@@ -2393,6 +2394,17 @@ namespace z3 {
             unsigned h() const { return m_h; }
         };
         optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
+        optimize(optimize& o):object(o)  {
+            Z3_optimize_inc_ref(o.ctx(), o.m_opt);
+            m_opt = o.m_opt;
+        }
+        optimize& operator=(optimize const& o) {
+            Z3_optimize_inc_ref(o.ctx(), o.m_opt);
+            Z3_optimize_dec_ref(ctx(), m_opt);
+            m_opt = o.m_opt;
+            m_ctx = o.m_ctx;
+            return *this;
+        }
         ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
         operator Z3_optimize() const { return m_opt; }
         void add(expr const& e) {
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 c2c257f43..981fd801f 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -394,7 +394,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());
         }
     }
@@ -619,7 +619,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/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index dddca492b..a23d654b0 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -108,7 +108,9 @@ public:
 #endif
     }
     ~line_reader() {
-        fclose(m_file);
+        if (m_file != nullptr){
+            fclose(m_file);
+        }
     }
 
     bool operator()() { return m_ok; }
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/smt_context.cpp b/src/smt/smt_context.cpp
index 12c64c404..14a19f824 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -627,10 +627,7 @@ namespace smt {
     */
     void context::remove_parents_from_cg_table(enode * r1) {
         // Remove parents from the congruence table
-        enode_vector::iterator it  = r1->begin_parents();
-        enode_vector::iterator end = r1->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : r1->get_parents()) {
 #if 0
             {
                 static unsigned num_eqs = 0;
@@ -675,10 +672,7 @@ namespace smt {
     */
     void context::reinsert_parents_into_cg_table(enode * r1, enode * r2, enode * n1, enode * n2, eq_justification js) {
         enode_vector & r2_parents  = r2->m_parents;
-        enode_vector::iterator it  = r1->begin_parents();
-        enode_vector::iterator end = r1->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : r1->get_parents()) {
             if (!parent->is_marked())
                 continue;
             parent->unset_mark();
@@ -1008,10 +1002,7 @@ namespace smt {
         r2->m_parents.shrink(r2_num_parents);
 
         // try to reinsert parents of r1 that are not cgr
-        it  = r1->begin_parents();
-        end = r1->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : r1->get_parents()) {
             TRACE("add_eq_parents", tout << "visiting: #" << parent->get_owner_id() << "\n";);
             if (parent->is_cgc_enabled()) {
                 enode * cg     = parent->m_cg;
@@ -1206,10 +1197,7 @@ namespace smt {
     bool context::is_diseq_slow(enode * n1, enode * n2) const {
         if (n1->get_num_parents() > n2->get_num_parents())
             std::swap(n1, n2);
-        enode_vector::iterator it  = n1->begin_parents();
-        enode_vector::iterator end = n1->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : n1->get_parents()) {
             if (parent->is_eq() && is_relevant(parent->get_owner()) && get_assignment(enode2bool_var(parent)) == l_false &&
                 ((parent->get_arg(0)->get_root() == n1->get_root() && parent->get_arg(1)->get_root() == n2->get_root()) ||
                  (parent->get_arg(1)->get_root() == n1->get_root() && parent->get_arg(0)->get_root() == n2->get_root()))) {
@@ -1241,10 +1229,7 @@ namespace smt {
             return false;
         if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
             TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";);
-            enode_vector::iterator it1  = r1->begin_parents();
-            enode_vector::iterator end1 = r1->end_parents();
-            for (; it1 != end1; ++it1) {
-                enode * p1        = *it1;
+            for (enode* p1 : r1->get_parents()) {
                 if (!is_relevant(p1))
                     continue;
                 if (p1->is_eq())
@@ -1254,10 +1239,7 @@ namespace smt {
                 func_decl * f     = p1->get_decl();
                 TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";);
                 unsigned num_args = p1->get_num_args();
-                enode_vector::iterator it2  = r2->begin_parents();
-                enode_vector::iterator end2 = r2->end_parents();
-                for (; it2 != end2; ++it2) {
-                    enode * p2  = *it2;
+                for (enode * p2 : r2->get_parents()) {
                     if (!is_relevant(p2))
                         continue;
                     if (p2->is_eq())
@@ -1295,10 +1277,7 @@ namespace smt {
             }
             almost_cg_table & table = *(m_almost_cg_tables[depth]);
             table.reset(r1, r2);
-            enode_vector::iterator it1  = r1->begin_parents();
-            enode_vector::iterator end1 = r1->end_parents();
-            for (; it1 != end1; ++it1) {
-                enode * p1        = *it1;
+            for (enode* p1 : r1->get_parents()) {
                 if (!is_relevant(p1))
                     continue;
                 if (p1->is_eq())
@@ -1309,10 +1288,7 @@ namespace smt {
             }
             if (table.empty())
                 return false;
-            enode_vector::iterator it2  = r2->begin_parents();
-            enode_vector::iterator end2 = r2->end_parents();
-            for (; it2 != end2; ++it2) {
-                enode * p2 = *it2;
+            for (enode * p2 : r2->get_parents()) {
                 if (!is_relevant(p2))
                     continue;
                 if (p2->is_eq())
@@ -1519,10 +1495,7 @@ namespace smt {
         }
         TRACE("push_new_th_diseqs", tout << "#" << r->get_owner_id() << " v" << v << "\n";);
         theory_id th_id = th->get_id();
-        enode_vector::iterator it  = r->begin_parents();
-        enode_vector::iterator end = r->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode * parent : r->get_parents()) {
             CTRACE("parent_bug", parent == 0, tout << "#" << r->get_owner_id() << ", num_parents: " << r->get_num_parents() << "\n"; display(tout););
             if (parent->is_eq()) {
                 bool_var bv = get_bool_var_of_id(parent->get_owner_id());
@@ -2215,9 +2188,7 @@ namespace smt {
                     TRACE("cached_generation", tout << "caching: #" << n->get_id() << " " << e->get_generation() << "\n";);
                     m_cached_generation.insert(n, e->get_generation());
                 }
-                unsigned num_args = to_app(n)->get_num_args();
-                for (unsigned i = 0; i < num_args; i++) {
-                    expr * arg = to_app(n)->get_arg(i);
+                for (expr * arg : *to_app(n)) {
                     if (is_app(arg) || is_quantifier(arg))
                         todo.push_back(arg);
                 }
@@ -4257,10 +4228,7 @@ namespace smt {
             theory_var_list * l = n->get_th_var_list();
             theory_id th_id     = l->get_th_id();
 
-            enode_vector::const_iterator it  = n->begin_parents();
-            enode_vector::const_iterator end = n->end_parents();
-            for (; it != end; ++it) {
-                enode * parent = *it;
+            for (enode* parent : n->get_parents()) {
                 family_id fid = parent->get_owner()->get_family_id();
                 if (fid != th_id && fid != m_manager.get_basic_family_id()) {
                     TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";);
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f4540ffc1..a6b881d10 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -341,10 +341,7 @@ namespace smt {
     }
 
     void context::display_parent_eqs(std::ostream & out, enode * n) const {
-        enode_vector::iterator it  = n->begin_parents();
-        enode_vector::iterator end = n->end_parents();
-        for (; it != end; ++it) {
-            enode * parent = *it;
+        for (enode* parent : n->get_parents()) {
             if (parent->is_eq())
                 display_eq_detail(out, parent);
         }
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index df6309424..6c8d156b4 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -216,15 +216,28 @@ namespace smt {
             return m_args;
         }
 
-        class args {
+        class const_args {
             enode const& n;
         public:
-            args(enode const& n):n(n) {}
-            args(enode const* n):n(*n) {}
-            enode_vector::const_iterator begin() const { return n.get_args(); }
-            enode_vector::const_iterator end() const { return n.get_args() + n.get_num_args(); }
+            const_args(enode const& n):n(n) {}
+            const_args(enode const* n):n(*n) {}
+            enode_vector::const_iterator begin() const { return n.m_args; }
+            enode_vector::const_iterator end() const { return n.m_args + n.get_num_args(); }
         };
 
+        class args {
+            enode & n;
+        public:
+            args(enode & n):n(n) {}
+            args(enode * n):n(*n) {}
+            enode_vector::iterator begin() const { return n.m_args; }
+            enode_vector::iterator end() const { return n.m_args + n.get_num_args(); }
+        };
+
+        const_args get_const_args() const { return const_args(this); }
+
+        // args get_args() { return args(this); }
+
         // unsigned get_id() const { 
         //    return m_id; 
         // }
@@ -294,15 +307,27 @@ namespace smt {
             return m_commutative;
         }
 
-        class parents {
+        class const_parents {
             enode const& n;
         public:
-            parents(enode const& _n):n(_n) {}
-            parents(enode const* _n):n(*_n) {}
+            const_parents(enode const& _n):n(_n) {}
+            const_parents(enode const* _n):n(*_n) {}
             enode_vector::const_iterator begin() const { return n.begin_parents(); }
             enode_vector::const_iterator end() const { return n.end_parents(); }
         };
 
+        class parents {
+            enode& n;
+        public:
+            parents(enode & _n):n(_n) {}
+            parents(enode * _n):n(*_n) {}
+            enode_vector::iterator begin() const { return n.begin_parents(); }
+            enode_vector::iterator end() const { return n.end_parents(); }
+        };
+
+        parents get_parents() { return parents(this); }
+
+        const_parents get_const_parents() const { return const_parents(this); }
 
         unsigned get_num_parents() const {
             return m_parents.size();
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 6d408b1e3..992a87dab 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 805a8321a..89196808f 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -1520,7 +1520,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 77da1d90a..acd75d663 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -264,8 +264,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) {}
     
diff --git a/src/util/lp/permutation_matrix.h b/src/util/lp/permutation_matrix.h
index 3c89b3646..8e664bba0 100644
--- a/src/util/lp/permutation_matrix.h
+++ b/src/util/lp/permutation_matrix.h
@@ -132,7 +132,7 @@ class permutation_matrix : public tail_matrix<T, X> {
 
         unsigned size() const { return static_cast<unsigned>(m_rev.size()); }
 
-        unsigned * values() const { return m_permutation; }
+        unsigned * values() const { return m_permutation.c_ptr(); }
 
         void resize(unsigned size) {
             unsigned old_size = m_permutation.size();
diff --git a/src/util/smt2_util.cpp b/src/util/smt2_util.cpp
index 8358c67ac..365d8fe70 100644
--- a/src/util/smt2_util.cpp
+++ b/src/util/smt2_util.cpp
@@ -34,6 +34,16 @@ bool is_smt2_quoted_symbol(char const * s) {
     if ('0' <= s[0] && s[0] <= '9')
         return true;
     unsigned len = static_cast<unsigned>(strlen(s));
+    if (len >= 2 && s[0] == '|' && s[len-1] == '|') {
+        for (unsigned i = 1; i + 1 < len; i++) {
+            if (s[i] == '\\' && i + 2 < len && (s[i+1] == '\\' || s[i+1] == '|')) {
+                i++;
+            }
+            else if (s[i] == '\\' || s[i] == '|') 
+                return true;
+        }
+        return false;
+    }
     for (unsigned i = 0; i < len; i++)
         if (!is_smt2_simple_symbol_char(s[i]))
             return true;