diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp
index 832c1d0bc..8feb217db 100644
--- a/src/ast/for_each_expr.cpp
+++ b/src/ast/for_each_expr.cpp
@@ -109,9 +109,9 @@ bool has_skolem_functions(expr * n) {
 
 subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {}
 subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); }
-subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); }
-subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); }
-subterms::iterator::iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
+subterms::iterator subterms::begin() const { return iterator(* this, m_esp, m_vp, true); }
+subterms::iterator subterms::end() const { return iterator(*this, nullptr, nullptr, false); }
+subterms::iterator::iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
     if (!esp)
         m_esp = &m_es;
     else
diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h
index 0ba0dc992..77b01e939 100644
--- a/src/ast/for_each_expr.h
+++ b/src/ast/for_each_expr.h
@@ -186,7 +186,7 @@ public:
         expr_mark         m_visited;   
         expr_mark*        m_visitedp = nullptr;
     public:
-        iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
+        iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
         expr* operator*();
         iterator operator++(int);
         iterator& operator++();
@@ -198,8 +198,8 @@ public:
     static subterms ground(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
     static subterms all(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
     static subterms ground(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
-    iterator begin();
-    iterator end();
+    iterator begin() const;
+    iterator end() const;
 };
 
 class subterms_postorder {
diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp
index ce98a6203..52da9e823 100644
--- a/src/sat/smt/synth_solver.cpp
+++ b/src/sat/smt/synth_solver.cpp
@@ -37,15 +37,18 @@ namespace synth {
         
     	auto * n = expr2enode(e->get_arg(0));
 	expr_ref_vector repr(m);
-	euf::enode_vector todo;
-        auto has_rep = [&](euf::enode* n) { return !!repr.get(n->get_root_id(), nullptr); };
         auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); };
+        auto has_rep = [&](euf::enode* n) { return !!get_rep(n); };
+        auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); };
+
+        euf::enode_vector todo;                
+        
 	for (unsigned i = 1; i < e->get_num_args(); ++i) {
 	    expr * arg = e->get_arg(i);
 	    auto * narg = expr2enode(arg);
 	    todo.push_back(narg);
-	    repr.setx(narg->get_root_id(), arg);
-	}
+	    set_rep(narg, arg);
+        }
 	for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) {
 	    auto * nn = todo[i];
 	    for (auto * p : euf::enode_parents(nn)) {
@@ -56,8 +59,8 @@ namespace synth {
 		    for (auto * ch : euf::enode_args(p))
                         args.push_back(get_rep(ch));
                     app * papp = m.mk_app(p->get_decl(), args);
-		    repr.setx(p->get_root_id(), papp);
-		    todo.push_back(p);
+		    set_rep(p, papp);
+                    todo.push_back(p);
 		}
 	    }
 	}
diff --git a/src/util/util.h b/src/util/util.h
index 6d4efb671..180c0a864 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -363,7 +363,7 @@ void set_fatal_error_handler(void (*pfn)(int error_code));
 
 
 template<typename S, typename T>
-bool any_of(S& set, T const& p) {
+bool any_of(S const & set, T const& p) {
     for (auto const& s : set)
         if (p(s))
             return true;
@@ -371,7 +371,7 @@ bool any_of(S& set, T const& p) {
 }
 
 template<typename S, typename T>
-bool all_of(S& set, T const& p) {
+bool all_of(S const & set, T const& p) {
     for (auto const& s : set)
         if (!p(s))
             return false;