diff --git a/include/mockturtle/algorithms/window_rewriting.hpp b/include/mockturtle/algorithms/window_rewriting.hpp
index da6d2743b..95dfe1b78 100644
--- a/include/mockturtle/algorithms/window_rewriting.hpp
+++ b/include/mockturtle/algorithms/window_rewriting.hpp
@@ -51,6 +51,27 @@ struct window_rewriting_params
   uint64_t cut_size{6};
   uint64_t num_levels{5};
 
+  /* Level information guides the windowing construction and as such impacts QoR:
+     -- dont_update: fastest, but levels are wrong (QoR degrades)
+     -- eager: fast, some levels are wrong
+     -- precise: fast, all levels are correct (best QoR)
+     -- recompute: slow, same as precise (used only for debugging)
+  */
+  enum
+  {
+    /* do not update any levels */
+    dont_update,
+    /* eagerly update the levels of changed nodes but avoid
+       topological sorting (some levels will be wrong) */
+    eager,
+    /* precisely update the levels of changed nodes bottom-to-top and
+       in topological order */
+    precise,
+    /* recompute all levels (also precise, but more expensive to
+       compute) */
+    recompute,
+  } level_update_strategy = dont_update;
+
   bool filter_cyclic_substitutions{false};
 }; /* window_rewriting_params */
 
@@ -77,6 +98,9 @@ struct window_rewriting_stats
   /*! \brief Time for encoding index_list. */
   stopwatch<>::duration time_encode{0};
 
+  /*! \brief Time for detecting cycles. */
+  stopwatch<>::duration time_cycle{0};
+
   /*! \brief Total number of calls to the resub. engine. */
   uint64_t num_substitutions{0};
   uint64_t num_restrashes{0};
@@ -93,6 +117,7 @@ struct window_rewriting_stats
     time_topo_sort += other.time_topo_sort;
     time_encode += other.time_encode;
     num_substitutions += other.num_substitutions;
+    num_restrashes += other.num_restrashes;
     num_windows += other.num_windows;
     gain += other.gain;
     return *this;
@@ -177,20 +202,24 @@ class window_rewriting_impl
     : ntk( ntk )
     , ps( ps )
     , st( st )
+    /* initialize levels to network depth */
+    , levels( ntk.depth() )
   {
     auto const update_level_of_new_node = [&]( const auto& n ) {
-      ntk.resize_levels();
-      update_node_level( n );
+      stopwatch t( st.time_total );
+      update_levels( n );
     };
 
     auto const update_level_of_existing_node = [&]( node const& n, const auto& old_children ) {
       (void)old_children;
-      ntk.resize_levels();
-      update_node_level( n );
+      stopwatch t( st.time_total );
+      update_levels( n );
     };
 
     auto const update_level_of_deleted_node = [&]( node const& n ) {
+      stopwatch t( st.time_total );
       assert( ntk.fanout_size( n ) == 0u );
+      assert( ntk.is_dead( n ) );
       ntk.set_level( n, -1 );
     };
 
@@ -205,7 +234,7 @@ class window_rewriting_impl
 
     create_window_impl windowing( ntk );
     uint32_t const size = ntk.size();
-    for ( uint32_t n = 0u; n < std::min( size, ntk.size() ); ++n )
+    for ( uint32_t n = 0u; n < size; ++n )
     {
       if ( ntk.is_constant( n ) || ntk.is_ci( n ) || ntk.is_dead( n ) )
       {
@@ -247,6 +276,9 @@ class window_rewriting_impl
         uint32_t counter{0};
         ++st.num_substitutions;
 
+        /* ensure that no dead nodes are reachable */
+        assert( count_reachable_dead_nodes( ntk ) == 0u );
+
         std::list<std::pair<node, signal>> substitutions;
         insert( ntk, std::begin( signals ), std::end( signals ), *il_opt,
                 [&]( signal const& _new )
@@ -260,13 +292,19 @@ class window_rewriting_impl
 
                   /* ensure that _old is not in the TFI of _new */
                   // assert( !is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ) );
-                  if ( ps.filter_cyclic_substitutions && is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ) )
+                  if ( ps.filter_cyclic_substitutions &&
+                       call_with_stopwatch( st.time_window, [&](){ return is_contained_in_tfi( ntk, ntk.get_node( _new ), ntk.get_node( _old ) ); }) )
                   {
                     std::cout << "undo resubstitution " << ntk.get_node( _old ) << std::endl;
-                    if ( ntk.fanout_size( ntk.get_node( _new ) ) == 0u )
+                    substitutions.emplace_back( std::make_pair( ntk.get_node( _old ), ntk.is_complemented( _old ) ? !_new : _new ) );                    
+                    for ( auto it = std::rbegin( substitutions ); it != std::rend( substitutions ); ++it )
                     {
-                      ntk.take_out_node( ntk.get_node( _new ) );
+                      if ( ntk.fanout_size( ntk.get_node( it->second ) ) == 0u )
+                      {
+                        ntk.take_out_node( ntk.get_node( it->second ) );
+                      }
                     }
+                    substitutions.clear();
                     return false;
                   }
 
@@ -274,11 +312,19 @@ class window_rewriting_impl
                   return true;
                 });
 
+        /* ensure that no dead nodes are reachable */
+        assert( count_reachable_dead_nodes( ntk ) == 0u );
         substitute_nodes( substitutions );
 
         /* recompute levels and depth */
-        // call_with_stopwatch( st.time_levels, [&]() { ntk.update_levels(); } );
-        update_depth();
+        if ( ps.level_update_strategy == window_rewriting_params::recompute )
+        {
+          call_with_stopwatch( st.time_levels, [&]() { ntk.update_levels(); } );
+        }
+        if ( ps.level_update_strategy != window_rewriting_params::dont_update )
+        {
+          update_depth();
+        }
 
         /* ensure that no dead nodes are reachable */
         assert( count_reachable_dead_nodes( ntk ) == 0u );
@@ -286,8 +332,12 @@ class window_rewriting_impl
         /* ensure that the network structure is still acyclic */
         assert( network_is_acylic( ntk ) );
 
-        /* ensure that the levels and depth is correct */
-        assert( check_network_levels( ntk ) );
+        if ( ps.level_update_strategy == window_rewriting_params::precise ||
+             ps.level_update_strategy == window_rewriting_params::recompute )
+        {
+          /* ensure that the levels and depth is correct */
+          assert( check_network_levels( ntk ) );
+        }
 
         /* update internal data structures in windowing */
         windowing.resize( ntk.size() );
@@ -370,7 +420,7 @@ class window_rewriting_impl
                                                {
                                                  ntk.decr_fanout_size( nn );
                                                }
-                                               /* remove the node if it's fanout_size becomes 0 */
+                                               /* remove the node if its fanout_size becomes 0 */
                                                if ( ntk.fanout_size( nn ) == 0 )
                                                {
                                                  ntk.take_out_node( nn );
@@ -399,24 +449,27 @@ class window_rewriting_impl
       auto const [old_node, new_signal] = substitutions.front();
       substitutions.pop_front();
 
-      // for ( auto index = 1u; index < _storage->nodes.size(); ++index )
-      const auto parents = ntk.fanout( old_node );
-      for ( auto index : parents )
+      for ( auto index : ntk.fanout( old_node ) )
       {
         /* skip CIs and dead nodes */
         if ( ntk.is_dead( index ) )
+        {
           continue;
+        }
 
         /* skip nodes that will be deleted */
         if ( std::find_if( std::begin( substitutions ), std::end( substitutions ),
                            [&index]( auto s ){ return s.first == index; } ) != std::end( substitutions ) )
+        {
           continue;
+        }
 
         /* replace in node */
         if ( const auto repl = ntk.replace_in_node( index, old_node, new_signal ); repl )
         {
           ntk.incr_fanout_size( ntk.get_node( repl->second ) );
           substitutions.emplace_back( *repl );
+          ++st.num_restrashes;
         }
       }
 
@@ -442,16 +495,102 @@ class window_rewriting_impl
 
       /* decrement fanout_size when released from substitution list */
       ntk.decr_fanout_size( ntk.get_node( new_signal ) );
+      if ( ntk.fanout_size( ntk.get_node( new_signal ) ) == 0 )
+      {
+        ntk.take_out_node( ntk.get_node( new_signal ) );
+      }
     }
 
     ntk._events->on_delete.pop_back();
   }
 
-  /* recursively update the node levels and the depth of the critical path */
-  void update_node_level( node const& n )
+  void update_levels( node const& n )
   {
-    uint32_t const curr_level = ntk.level( n );
+    ntk.resize_levels();
+    if ( ps.level_update_strategy == window_rewriting_params::precise )
+    {
+      call_with_stopwatch( st.time_levels, [&]() { update_node_level_precise( n ); } );
+    }
+    else if ( ps.level_update_strategy == window_rewriting_params::eager )
+    {
+      call_with_stopwatch( st.time_levels, [&]() { update_node_level_eager( n ); } );
+    }
+
+    /* levels can be wrong until substitute_nodes has finished */
+    // assert( check_network_levels( ntk ) );
+  }
+
+  /* precisely update node levels using an iterative topological sorting approach */
+  void update_node_level_precise( node const& n )
+  {
+    assert( count_reachable_dead_nodes_from_node( ntk, n ) == 0u );
+    // assert( count_nodes_with_dead_fanins( ntk, n ) == 0u );
+
+    /* compute level of current node */
+    uint32_t level_offset{0};
+    ntk.foreach_fanin( n, [&]( signal const& fi ){
+      level_offset = std::max( ntk.level( ntk.get_node( fi ) ), level_offset );
+    });
+    ++level_offset;
+
+    /* add node into levels */
+    if ( levels.size() < 1u )
+    {
+      levels.resize( 1u );
+    }
+    levels[0].emplace_back( n );
+
+    for ( uint32_t level_index = 0u; level_index < levels.size(); ++level_index )
+    {
+      if ( levels[level_index].empty() )
+        continue;
+
+      for ( uint32_t node_index = 0u; node_index < levels[level_index].size(); ++node_index )
+      {
+        node const p = levels[level_index][node_index];
+
+        /* recompute level of this node */
+        uint32_t lvl{0};
+        ntk.foreach_fanin( p, [&]( signal const& fi ){
+          if ( ntk.is_dead( ntk.get_node( fi ) ) )
+            return;
+
+          lvl = std::max( ntk.level( ntk.get_node( fi ) ), lvl );
+          return;
+        });
+        ++lvl;
+        assert( lvl > 0 );
 
+        /* update level and add fanouts to levels[.] if the recomputed
+           level is different from the current level */
+        if ( lvl != ntk.level( p ) )
+        {
+          ntk.set_level( p, lvl );
+          ntk.foreach_fanout( p, [&]( node const& fo ){
+            assert( std::max( ntk.level( fo ), lvl + 1 ) >= level_offset );
+            uint32_t const pos = std::max( ntk.level( fo ), lvl + 1 ) - level_offset;
+            assert( pos >= 0u );
+            assert( pos >= level_index );
+            if ( levels.size() <= pos )
+            {
+              levels.resize( std::max( uint32_t( levels.size() << 1 ), pos + 1 ) );
+            }
+            levels[pos].emplace_back( fo );
+          });
+        }
+      }
+
+      /* clean the level */
+      levels[level_index].clear();
+    }
+    levels.clear();
+  }
+
+  /* eagerly update the node levels without topologically sorting (may
+     stack-overflow if the network is deep)*/
+  void update_node_level_eager( node const& n )
+  {
+    uint32_t const curr_level = ntk.level( n );
     uint32_t max_level = 0;
     ntk.foreach_fanin( n, [&]( const auto& f ) {
       auto const p = ntk.get_node( f );
@@ -469,21 +608,21 @@ class window_rewriting_impl
       ntk.foreach_fanout( n, [&]( const auto& p ) {
         if ( !ntk.is_dead( p ) )
         {
-          update_node_level( p );
+          update_node_level_eager( p );
         }
       } );
     }
   }
 
+  /* update network depth (needs level information!) */
   void update_depth()
   {
+    stopwatch t( st.time_levels );
+
     uint32_t max_level{0};
-    ntk.foreach_co( [&]( signal s ){
+    ntk.foreach_co( [&]( signal const& s ){
       assert( !ntk.is_dead( ntk.get_node( s ) ) );
-      if ( ntk.level( ntk.get_node( s ) ) > max_level )
-      {
-        max_level = ntk.level( ntk.get_node( s ) );
-      }
+      max_level = std::max( ntk.level( ntk.get_node( s ) ), max_level );
     });
 
     if ( ntk.depth() != max_level )
@@ -496,9 +635,11 @@ class window_rewriting_impl
   Ntk& ntk;
   window_rewriting_params ps;
   window_rewriting_stats& st;
-}; /* window_rewriting_impl */
 
-} /* detail */
+  std::vector<std::vector<node>> levels;
+};
+
+} /* namespace detail */
 
 template<class Ntk>
 void window_rewriting( Ntk& ntk, window_rewriting_params const& ps = {}, window_rewriting_stats* pst = nullptr )
diff --git a/include/mockturtle/utils/debugging_utils.hpp b/include/mockturtle/utils/debugging_utils.hpp
index 3137619da..8639a4e2d 100644
--- a/include/mockturtle/utils/debugging_utils.hpp
+++ b/include/mockturtle/utils/debugging_utils.hpp
@@ -38,6 +38,35 @@
 namespace mockturtle
 {
 
+template<typename Ntk>
+inline void print( Ntk const& ntk )
+{
+  using node = typename Ntk::node;
+  using signal = typename Ntk::signal;
+
+  for ( uint32_t n = 0; n < ntk.size(); ++n )
+  {
+    std::cout << n;
+
+    if ( ntk.is_constant( n ) || ntk.is_pi( n ) )
+    {
+      std::cout << std::endl;
+      continue;
+    }
+
+    std::cout << " = ";
+
+    ntk.foreach_fanin( n, [&]( signal const& fi ){
+      std::cout << ( ntk.is_complemented( fi ) ? "~" : "" ) << ntk.get_node( fi ) << " ";
+    });
+    std::cout << " ; [level = " << int32_t( ntk.level( n ) ) << "]" << " [dead = " << ntk.is_dead( n ) << "]" << " [ref = " << ntk.fanout_size( n ) << "]" << std::endl;
+  }
+
+  ntk.foreach_co( [&]( signal const& s ){
+    std::cout << "o " << ( ntk.is_complemented( s ) ? "~" : "" ) << ntk.get_node( s ) << std::endl;
+  });
+}
+
 template<typename Ntk>
 inline uint64_t count_dead_nodes( Ntk const& ntk )
 {
@@ -130,6 +159,114 @@ inline uint64_t count_reachable_dead_nodes( Ntk const& ntk )
 namespace detail
 {
 
+template<typename Ntk>
+void count_reachable_dead_nodes_from_node_recur( Ntk const& ntk, typename Ntk::node const& n, std::vector<typename Ntk::node>& nodes )
+{
+  using node = typename Ntk::node;
+
+  if ( ntk.current_color() == ntk.color( n ) )
+  {
+    return;
+  }
+
+  if ( ntk.is_dead( n ) )
+  {
+    if ( std::find( std::begin( nodes ), std::end( nodes ), n ) == std::end( nodes ) )
+    {
+      nodes.push_back( n );
+    }
+  }
+
+  ntk.paint( n );
+  ntk.foreach_fanout( n, [&]( node const& fo ){
+    count_reachable_dead_nodes_from_node_recur( ntk, fo, nodes );
+  });
+}
+
+} /* namespace detail */
+
+template<typename Ntk>
+inline uint64_t count_reachable_dead_nodes_from_node( Ntk const& ntk, typename Ntk::node const& n )
+{
+  static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+  static_assert( has_color_v<Ntk>, "Ntk does not implement the color function" );
+  static_assert( has_current_color_v<Ntk>, "Ntk does not implement the current_color function" );
+  static_assert( has_foreach_co_v<Ntk>, "Ntk does not implement the foreach_co function" );
+  static_assert( has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin function" );
+  static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node function" );
+  // static_assert( has_is_dead_v<Ntk>, "Ntk does not implement the is_dead function" );
+  static_assert( has_new_color_v<Ntk>, "Ntk does not implement the new_color function" );
+  static_assert( has_paint_v<Ntk>, "Ntk does not implement the paint function" );
+
+  using node = typename Ntk::node;
+  using signal = typename Ntk::signal;
+
+  ntk.new_color();
+
+  std::vector<node> dead_nodes;
+  detail::count_reachable_dead_nodes_from_node_recur( ntk, n, dead_nodes );
+
+  return dead_nodes.size();
+}
+
+namespace detail
+{
+
+template<typename Ntk>
+void count_nodes_with_dead_fanins_recur( Ntk const& ntk, typename Ntk::node const& n, std::vector<typename Ntk::node>& nodes )
+{
+  using node = typename Ntk::node;
+  using signal = typename Ntk::signal;
+
+  if ( ntk.current_color() == ntk.color( n ) )
+  {
+    return;
+  }
+  ntk.paint( n );
+
+  ntk.foreach_fanin( n, [&]( signal const& s ){
+    if ( ntk.is_dead( ntk.get_node( s ) ) )
+    {
+      if ( std::find( std::begin( nodes ), std::end( nodes ), n ) == std::end( nodes ) )
+      {
+        nodes.push_back( n );
+      }
+    }
+  });
+
+  ntk.foreach_fanout( n, [&]( node const& fo ){
+    count_nodes_with_dead_fanins_recur( ntk, fo, nodes );
+  });
+}
+
+} /* namespace detail */
+
+template<typename Ntk>
+uint64_t count_nodes_with_dead_fanins( Ntk const& ntk, typename Ntk::node const& n )
+{
+  static_assert( is_network_type_v<Ntk>, "Ntk is not a network type" );
+  static_assert( has_color_v<Ntk>, "Ntk does not implement the color function" );
+  static_assert( has_current_color_v<Ntk>, "Ntk does not implement the current_color function" );
+  static_assert( has_foreach_co_v<Ntk>, "Ntk does not implement the foreach_co function" );
+  static_assert( has_foreach_fanin_v<Ntk>, "Ntk does not implement the foreach_fanin function" );
+  static_assert( has_get_node_v<Ntk>, "Ntk does not implement the get_node function" );
+  // static_assert( has_is_dead_v<Ntk>, "Ntk does not implement the is_dead function" );
+  static_assert( has_new_color_v<Ntk>, "Ntk does not implement the new_color function" );
+  static_assert( has_paint_v<Ntk>, "Ntk does not implement the paint function" );
+
+  using node = typename Ntk::node;
+
+  ntk.new_color();
+
+  std::vector<node> nodes_with_dead_fanins;
+  detail::count_nodes_with_dead_fanins_recur( ntk, n, nodes_with_dead_fanins );
+
+  return nodes_with_dead_fanins.size();
+}
+
+namespace detail
+{
+
 template<typename Ntk>
 bool network_is_acylic_recur( Ntk const& ntk, typename Ntk::node const& n )
 {
diff --git a/include/mockturtle/utils/window_utils.hpp b/include/mockturtle/utils/window_utils.hpp
index 4e7537111..2d08a6416 100644
--- a/include/mockturtle/utils/window_utils.hpp
+++ b/include/mockturtle/utils/window_utils.hpp
@@ -664,7 +664,7 @@ void expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::node> const&
 namespace detail
 {
 
-template<typename Ntk>
+template<typename Ntk, bool auto_resize = true>
 void levelized_expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::node> const& inputs, std::vector<typename Ntk::node>& nodes,
                                    std::vector<std::vector<typename Ntk::node>>& levels )
 {
@@ -685,6 +685,13 @@ void levelized_expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::nod
   {
     uint32_t const node_level = ntk.level( i );
     ntk.paint( i );
+    if constexpr ( auto_resize )
+    {
+      if ( levels.size() <= node_level )
+      {
+        levels.resize( std::max( uint32_t( 2*levels.size() ), node_level ) );
+      }
+    }
     levels.at( node_level ).push_back( i );
     if ( std::find( std::begin( used ), std::end( used ), node_level ) == std::end( used ) )
     {
@@ -697,6 +704,13 @@ void levelized_expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::nod
   {
     uint32_t const node_level = ntk.level( n );
     ntk.paint( n );
+    if constexpr ( auto_resize )
+    {
+      if ( levels.size() <= node_level )
+      {
+        levels.resize( std::max( uint32_t( 2 * levels.size() ), node_level ) );
+      }
+    }
     levels.at( node_level ).push_back( n );
     if ( std::find( std::begin( used ), std::end( used ), node_level ) == std::end( used ) )
     {
@@ -733,6 +747,13 @@ void levelized_expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::nod
           /* update data structured */
           uint32_t const node_level = ntk.level( fo );
           ntk.paint( fo );
+          if constexpr ( auto_resize )
+          {
+            if ( levels.size() <= node_level )
+            {
+              levels.resize( std::max( uint32_t( 2*levels.size() ), node_level ) );
+            }
+          }
           levels.at( node_level ).push_back( fo );
           if ( std::find( std::begin( used ), std::end( used ), node_level ) == std::end( used ) )
           {
@@ -777,11 +798,11 @@ void levelized_expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::nod
  * - `new_color`
  * - `paint`
  */
-template<typename Ntk>
+template<typename Ntk, bool auto_resize = true>
 void levelized_expand_towards_tfo( Ntk const& ntk, std::vector<typename Ntk::node> const& inputs, std::vector<typename Ntk::node>& nodes )
 {
   std::vector<std::vector<typename Ntk::node>> levels;
-  detail::levelized_expand_towards_tfo( ntk, inputs, nodes, levels );
+  detail::levelized_expand_towards_tfo<Ntk, auto_resize>( ntk, inputs, nodes, levels );
 }
 
 namespace detail