diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 52623b461..bdd96b756 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -613,8 +613,15 @@ namespace smt {
             split_set pairs;
             auto [head, tail] = seq::split_membership(mem.m_str, mem.m_regex, m_sg, threshold, pairs);
 
+            if (!head) {
+                // gave up
+                SASSERT(!tail);
+                return;
+            }
+
+            SASSERT(tail);
+
             if (pairs.empty()) {
-                // no viable splits
                 literal_vector lits;
                 lits.push_back(mem.lit);
                 set_conflict(lits);
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index d52d9fe6d..b2c64f859 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -136,7 +136,7 @@ namespace smt {
         // private helpers
         void populate_nielsen_graph();
         void explain_nielsen_conflict();
-        void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
+        void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits) const;
         void set_conflict(literal_vector const& lits) {
             const enode_pair_vector eqs;
             set_conflict(eqs, lits);