diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index f6e51e8f5..05018df10 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1221,6 +1221,37 @@ static void string_values() {
     std::cout << s1 << "\n";
 }
 
+expr MakeStringConstant(context* context, std::string value) {
+    return context->string_val(value.c_str());
+}
+
+expr MakeStringFunction(context* c, std::string s) {
+    sort sort = c->string_sort();
+    symbol name = c->str_symbol(s.c_str());
+    return c->constant(name, sort);
+}
+
+static void string_issue_2298() {
+    context c;
+    solver s(c);
+    s.push();
+    expr func1 = MakeStringFunction(&c, "func1");
+    expr func2 = MakeStringFunction(&c, "func2");
+    
+    expr abc = MakeStringConstant(&c, "abc");
+    expr cde = MakeStringConstant(&c, "cde");
+    
+    expr length = func1.length();
+    expr five = c.int_val(5);
+    
+    s.add(func2 == abc || func1 == cde);
+    s.add(func2 == abc || func2 == cde);
+    s.add(length <= five);
+    
+    s.check();
+    s.pop();
+}
+
 int main() {
 
     try {
@@ -1272,6 +1303,7 @@ int main() {
         mk_model_example(); std::cout << "\n";
         recfun_example(); std::cout << "\n";
         string_values(); std::cout << "\n";
+        string_issue_2298(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index d9477e95d..051684dce 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -274,10 +274,7 @@ namespace smt {
 
         // Parent use-list
         if (this == m_root) {
-            enode_vector::const_iterator it2  = m_parents.begin();
-            enode_vector::const_iterator end2 = m_parents.end();
-            for (; it2 != end2; ++it2) {
-                enode const * parent = *it2;
+            for (enode* parent : m_parents) {
                 unsigned i = 0;
                 unsigned num_args = parent->get_num_args();
                 SASSERT(num_args > 0);
@@ -318,10 +315,7 @@ namespace smt {
         enode const * curr = m_root; 
         do {
             if (curr != m_root) {
-                enode_vector::const_iterator it  = curr->m_parents.begin();
-                enode_vector::const_iterator end = curr->m_parents.end();
-                for (; it != end; ++it) {
-                    enode * p = *it;
+                for (enode * p : curr->m_parents) {
                     if (!p->is_true_eq() && !m_root->contains_parent_congruent_to(p)) {
                         UNREACHABLE();
                     }
@@ -334,10 +328,7 @@ namespace smt {
     }
     
     bool enode::contains_parent_congruent_to(enode * p) const {
-        enode_vector::const_iterator it  = m_parents.begin();
-        enode_vector::const_iterator end = m_parents.end();
-        for (; it != end; ++it) {
-            enode * curr = *it;
+        for (enode* curr : m_parents) {
             if (congruent(curr, p))
                 return true;
         }