diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 82607452f..75b0c38e9 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -677,8 +677,22 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
     }
     // check if subsequence of a is in b.
     expr_ref_vector as(m()), bs(m());
-    m_util.str.get_concat(a, as);
-    m_util.str.get_concat(b, bs);
+    if (m_util.str.is_string(a, c)) {
+        for (unsigned i = 0; i < c.length(); ++i) {
+            as.push_back(m_util.str.mk_unit(m_util.str.mk_char(c, i)));
+        }
+    }
+    else {
+        m_util.str.get_concat(a, as);
+    }
+    if (m_util.str.is_string(b, d)) {
+        for (unsigned i = 0; i < d.length(); ++i) {
+            bs.push_back(m_util.str.mk_unit(m_util.str.mk_char(d, i)));
+        }
+    }
+    else {
+        m_util.str.get_concat(b, bs);
+    }
     bool all_values = true;
     TRACE("seq", tout << mk_pp(a, m()) << " contains " << mk_pp(b, m()) << "\n";);
    
@@ -719,7 +733,6 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
         }
     }
 
-
     if (as.empty()) {
         result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)));
         return BR_REWRITE2;
@@ -755,14 +768,10 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
         result = m().mk_true();
         return BR_DONE;
     }
-    bool all_units = true;
-    for (unsigned i = 0; i < bs.size(); ++i) { 
-        all_units = m_util.str.is_unit(bs[i].get());
-    }
-    for (unsigned i = 0; i < as.size(); ++i) { 
-        all_units = m_util.str.is_unit(as[i].get());
-    }
-    if (all_units) {
+
+    std::function<bool(expr*)> is_unit = [&](expr *e) { return m_util.str.is_unit(e); };
+
+    if (bs.forall(is_unit) && as.forall(is_unit)) {
         if (as.size() < bs.size()) {
             result = m().mk_false();
             return BR_DONE;
@@ -1595,6 +1604,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
     return BR_REWRITE3;
 }
 
+
 bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
     expr* a, *b;
     zstring s;
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index d0a17116a..02803a514 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -306,24 +306,31 @@ public:
     // prevent abuse:
     ref_vector & operator=(ref_vector const & other) = delete;
 
-    bool containsp(std::function<bool(T)>& predicate) const {
-        for (auto const& t : *this)
+    bool forall(std::function<bool(T*)>& predicate) const {
+        for (T* t : *this)
+            if (!predicate(t)) 
+                return false;
+        return true;
+    }
+
+    bool exists(std::function<bool(T*)>& predicate) const {
+        for (T* t : *this)
             if (predicate(t)) 
                 return true;
         return false;
     }
 
-    ref_vector filter_pure(std::function<bool(T)>& predicate) const {
+    ref_vector filter_pure(std::function<bool(T*)>& predicate) const {
         ref_vector result(m());
-        for (auto& t : *this)
+        for (T* t : *this)
             if (predicate(t)) 
                 result.push_back(t);
         return result;
     }
 
 #if 0
-    // TBD: not sure why some compilers complain here.
-    ref_vector& filter_update(std::function<bool(T)>& predicate) {
+    // TBD: 
+    ref_vector& filter_update(std::function<bool(T*)>& predicate) {
         unsigned j = 0;
         for (auto& t : *this)
             if (predicate(t)) 
@@ -334,23 +341,23 @@ public:
 #endif
 
     template <typename S>
-    vector<S> mapv_pure(std::function<S(T)>& f) const {
+    vector<S> mapv_pure(std::function<S(T*)>& f) const {
         vector<S> result;
-        for (auto& t : *this)
+        for (T* t : *this)
             result.push_back(f(t));
         return result;
     }
 
-    ref_vector map_pure(std::function<T(T)>& f) const {
+    ref_vector map_pure(std::function<T*(T*)>& f) const {
         ref_vector result(m());
-        for (auto& t : *this)
+        for (T* t : *this)
             result.push_back(f(t));
         return result;
     }
 
-    ref_vector& map_update(std::function<T(T)>& f)  {
+    ref_vector& map_update(std::function<T*(T*)>& f)  {
         unsigned j = 0;
-        for (auto& t : *this)
+        for (T* t : *this)
             set(j++, f(t));
         return *this;
     }