diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index b25f0c4ee..b0bf0462e 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -44,7 +44,7 @@ NSB review:
 
 namespace seq {
 
-    void deps_to_lits(dep_tracker deps, svector<enode_pair> &eqs, svector<sat::literal> &lits, vector<le, false>& les) {
+    void deps_to_lits(dep_tracker deps, svector<enode_pair> &eqs, svector<sat::literal> &lits, vector<le>& les) {
         vector<dep_source, false> vs;
         dep_manager::s_linearize(deps, vs);
         for (dep_source const &d : vs) {
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 7f41f9935..d56b4d6e7 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -362,7 +362,7 @@ namespace seq {
     void deps_to_lits(dep_tracker deps,
                       svector<enode_pair>& eqs,
                       svector<sat::literal>& lits,
-                      vector<le, false>& les);
+                      vector<le>& les);
 
     // string equality constraint: lhs = rhs
     // mirrors ZIPT's StrEq (both sides are regex-free snode trees)
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index bdac47d75..16f64886f 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -1262,7 +1262,7 @@ namespace smt {
         // conditional constraints: propagate with justification from dep_tracker
         enode_pair_vector eqs;
         literal_vector lits;
-        vector<seq::le, false> les;
+        vector<seq::le> les;
         seq::deps_to_lits(lc.m_dep, eqs, lits, les);
         for (auto const& d : les)
             lits.push_back(mk_le_literal(d));
@@ -1553,11 +1553,10 @@ namespace smt {
 
                 enode_pair_vector eqs;
                 literal_vector dep_lits;
-                vector<seq::le, false> dep_les;
-                for (unsigned idx : mem_indices) {
-                    if (mems[idx].m_dep)
-                        seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits, dep_les);
-                }
+                vector<seq::le> dep_les;
+                for (unsigned idx : mem_indices) 
+                    seq::deps_to_lits(mems[idx].m_dep, eqs, dep_lits, dep_les);
+                
                 for (auto const &d : dep_les)
                     dep_lits.push_back(mk_le_literal(d));