diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 75247762a..bde836752 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -3043,19 +3043,16 @@ namespace seq {
     // -----------------------------------------------------------------------
 
     bool nielsen_graph::apply_cycle_decomposition(nielsen_node* node) {
-        return false; // For now, disable
-        if (!node->backedge())
-            return false;
-
+        return false;
         // Look for a str_mem with a variable-headed string
         for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) {
             str_mem const& mem = node->str_mems()[mi];
-            if (!mem.m_str || !mem.m_regex) 
-                continue;
+            SASSERT(mem.well_formed());
             if (mem.is_primitive()) 
                 continue;
             euf::snode* first = mem.m_str->first();
-            if (!first || !first->is_var()) 
+            SASSERT(first);
+            if (!first->is_var())
                 continue;
 
             euf::snode* x = first;
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index 88d94c397..87ad3c852 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -584,7 +584,6 @@ namespace seq {
 
         // edges
         ptr_vector<nielsen_edge> m_outgoing;
-        nielsen_node*           m_backedge = nullptr;
         nielsen_edge*           m_parent_edge = nullptr;
 
         // status flags
@@ -651,9 +650,6 @@ namespace seq {
         ptr_vector<nielsen_edge> const& outgoing() const { return m_outgoing; }
         void add_outgoing(nielsen_edge* e) { m_outgoing.push_back(e); }
 
-        nielsen_node* backedge() const { return m_backedge; }
-        void set_backedge(nielsen_node* n) { m_backedge = n; }
-
         nielsen_edge* parent_edge() const { return m_parent_edge; }
         void set_parent_edge(nielsen_edge* e) { m_parent_edge = e; }
 
diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp
index fb580abcc..221a73fef 100644
--- a/src/smt/seq/seq_nielsen_pp.cpp
+++ b/src/smt/seq/seq_nielsen_pp.cpp
@@ -19,7 +19,6 @@ Author:
 #include "smt/seq/seq_nielsen.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/ast_pp.h"
-#include "ast/rewriter/seq_rewriter.h"
 #include "util/obj_hashtable.h"
 #include <sstream>
 
@@ -86,9 +85,6 @@ namespace seq {
             out << "\n";
         }
 
-        if (n->backedge())
-            out << "    backedge -> node[" << n->backedge()->id() << "]\n";
-
         return out;
     }
 
@@ -634,13 +630,7 @@ namespace seq {
 
                 out << "];\n";
             }
-
-            // backedge as dotted arrow
-            if (n->backedge())
-                out << "    " << n->id() << " -> " << n->backedge()->id()
-                    << " [style=dotted];\n";
         }
-
         out << "}\n";
         return out;
     }