diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 99de61703..aab4bcb21 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/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index aeaebc6bf..ade12de62 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -912,7 +912,7 @@ class smt2_printer {
                 var_name = mk_smt2_quoted_symbol (*it);
             }
             else {
-              var_name = it->str ();\
+                var_name = it->str ();          
             }
             buf.push_back(mk_seq1<format**,f2f>(m(), fs, fs+1, f2f(), var_name.c_str ()));
         }
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/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 608b7c63e..3f7966a73 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());
@@ -2197,9 +2170,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);
                 }
@@ -4228,10 +4199,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 f4f56df5d..615cd2512 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/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;