diff --git a/examples/prove.jl b/examples/prove.jl
index dfce791f..acac87d5 100644
--- a/examples/prove.jl
+++ b/examples/prove.jl
@@ -1,4 +1,4 @@
-# Sketch function for basic iterative saturation and extraction 
+# Sketch function for basic iterative saturation and extraction
 function prove(
   t,
   ex,
@@ -32,9 +32,9 @@ function test_equality(t, exprs...; params = SaturationParams(), g = EGraph())
   params = deepcopy(params)
   params.goal = (g::EGraph) -> in_same_class(g, ids...)
 
+  g.root = first(ids) # to allow extraction (for debugging)
   report = saturate!(g, t, params)
   goal_reached = params.goal(g)
-
   if !(report.reason === :saturated) && !goal_reached
     return false # failed to prove
   end
diff --git a/src/EGraphs/egraph.jl b/src/EGraphs/egraph.jl
index ad5dc41a..8bbc76e2 100644
--- a/src/EGraphs/egraph.jl
+++ b/src/EGraphs/egraph.jl
@@ -7,7 +7,7 @@
 
 The `modify!` function for EGraph Analysis can optionally modify the eclass
 `eclass` after it has been analyzed, typically by adding an e-node.
-It should be **idempotent** if no other changes occur to the EClass. 
+It should be **idempotent** if no other changes occur to the EClass.
 (See the [egg paper](https://dl.acm.org/doi/pdf/10.1145/3434304)).
 """
 function modify! end
@@ -25,7 +25,7 @@ function join end
 """
     make(g::EGraph{ExpressionType, AnalysisType}, n::VecExpr)::AnalysisType where {ExpressionType}
 
-Given an e-node `n`, `make` should return the corresponding analysis value. 
+Given an e-node `n`, `make` should return the corresponding analysis value.
 """
 function make end
 
@@ -42,7 +42,7 @@ they represent. The [`EGraph`](@ref) itself comes with pretty printing for human
 mutable struct EClass{D}
   const id::Id
   const nodes::Vector{VecExpr}
-  const parents::Vector{Pair{VecExpr,Id}}
+  parents::Vector{Pair{VecExpr,Id}} # the parent nodes and eclasses for upward merging
   data::Union{D,Nothing}
 end
 
@@ -65,10 +65,6 @@ function Base.show(io::IO, a::EClass)
   end
 end
 
-function addparent!(@nospecialize(a::EClass), n::VecExpr, id::Id)
-  push!(a.parents, (n => id))
-end
-
 
 function merge_analysis_data!(a::EClass{D}, b::EClass{D})::Tuple{Bool,Bool,Union{D,Nothing}} where {D}
   if !isnothing(a.data) && !isnothing(b.data)
@@ -123,9 +119,10 @@ mutable struct EGraph{ExpressionType,Analysis}
   memo::Dict{VecExpr,Id}
   "Hashcons the constants in the e-graph"
   constants::Dict{UInt64,Any}
-  "Nodes which need to be processed for rebuilding. The id is the id of the enode, not the canonical id of the eclass."
-  pending::Vector{Pair{VecExpr,Id}}
-  analysis_pending::UniqueQueue{Pair{VecExpr,Id}}
+  "E-classes whose parent nodes have to be reprocessed."
+  pending::Vector{Id}
+  "E-classes whose parent nodes have to be reprocessed for analysis values."
+  analysis_pending::Vector{Id}
   root::Id
   "a cache mapping signatures (function symbols and their arity) to e-classes that contain e-nodes with that function symbol."
   classes_by_op::Dict{IdKey,Vector{Id}}
@@ -146,8 +143,8 @@ function EGraph{ExpressionType,Analysis}(; needslock::Bool = false) where {Expre
     Dict{IdKey,EClass{Analysis}}(),
     Dict{VecExpr,Id}(),
     Dict{UInt64,Any}(),
-    Pair{VecExpr,Id}[],
-    UniqueQueue{Pair{VecExpr,Id}}(),
+    Vector{Id}(),
+    Vector{Id}(),
     0,
     Dict{IdKey,Vector{Id}}(),
     false,
@@ -198,9 +195,10 @@ function to_expr(g::EGraph, n::VecExpr)
 end
 
 function pretty_dict(g::EGraph)
-  d = Dict{Int,Vector{Any}}()
+  d = Dict{Int,Tuple{Vector{Any},Vector{Any}}}()
   for (class_id, eclass) in g.classes
-    d[class_id.val] = map(n -> to_expr(g, n), eclass.nodes)
+    # TODO do not show parent lists anymore (but useful for debugging)
+    d[class_id.val] = (map(n -> to_expr(g, n), eclass.nodes), map(pair -> to_expr(g, pair[1]) => Int(pair[2]), eclass.parents))
   end
   d
 end
@@ -209,8 +207,8 @@ export pretty_dict
 function Base.show(io::IO, g::EGraph)
   d = pretty_dict(g)
   t = "$(typeof(g)) with $(length(d)) e-classes:"
-  cs = map(sort!(collect(d); by = first)) do (k, vect)
-    "  $k => [$(Base.join(vect, ", "))]"
+  cs = map(sort!(collect(d); by = first)) do (k, (nodes, parents))
+    "  $k => [$(Base.join(nodes, ", "))] parents: [$(Base.join(parents, ", "))]"
   end
   print(io, Base.join([t; cs], "\n"))
 end
@@ -239,13 +237,13 @@ function lookup(g::EGraph, n::VecExpr)::Id
   canonicalize!(g, n)
 
   id = get(g.memo, n, zero(Id))
-  iszero(id) ? id : find(g, id)
+  iszero(id) ? id : find(g, id) # find necessary because g.memo values are not necessarily canonical
 end
 
 
 function add_class_by_op(g::EGraph, n, eclass_id)
   key = IdKey(v_signature(n))
-  vec = get!(g.classes_by_op, key, Vector{Id}())
+  vec = get!(Vector{Id}, g.classes_by_op, key)
   push!(vec, eclass_id)
 end
 
@@ -264,19 +262,23 @@ function add!(g::EGraph{ExpressionType,Analysis}, n::VecExpr, should_copy::Bool)
 
   id = push!(g.uf) # create new singleton eclass
 
+  # eclass.nodes, eclass.parents, and g.memo all have a reference to the same VecExpr for the new enode.
+  # The node must never be manipulated while it is contained in memo.
+  
   if v_isexpr(n)
     for c_id in v_children(n)
-      addparent!(g.classes[IdKey(c_id)], n, id)
+      push!(g.classes[IdKey(c_id)].parents, n => id)
     end
   end
 
   g.memo[n] = id
 
   add_class_by_op(g, n, id)
-  eclass = EClass{Analysis}(id, VecExpr[copy(n)], Pair{VecExpr,Id}[], make(g, n))
+  eclass = EClass{Analysis}(id, VecExpr[n], Id[], make(g, n))
   g.classes[IdKey(id)] = eclass
   modify!(g, eclass)
-  push!(g.pending, n => id)
+
+  # push!(g.pending, id) #  We just created a new eclass for a new node. No need to reprocess parents
 
   return id
 end
@@ -284,7 +286,7 @@ end
 
 """
 Extend this function on your types to do preliminary
-preprocessing of a symbolic term before adding it to 
+preprocessing of a symbolic term before adding it to
 an EGraph. Most common preprocessing techniques are binarization
 of n-ary terms and metadata stripping.
 """
@@ -293,14 +295,15 @@ function preprocess(e::Expr)
 end
 preprocess(x) = x
 
+addexpr!(::EGraph, se::EClass) = se.id # TODO: why do we need this?
+
 """
 Recursively traverse an type satisfying the `TermInterface` and insert terms into an
 [`EGraph`](@ref). If `e` has no children (has an arity of 0) then directly
 insert the literal into the [`EGraph`](@ref).
 """
 function addexpr!(g::EGraph, se)::Id
-  se isa EClass && return se.id
-  e = preprocess(se)
+  e = preprocess(se) # TODO: type stability issue?
 
   isexpr(e) || return add!(g, VecExpr(Id[Id(0), Id(0), Id(0), add_constant!(g, e)]), false)
 
@@ -341,16 +344,17 @@ function Base.union!(
     id_1, id_2 = id_2, id_1
   end
 
-  union!(g.uf, id_1.val, id_2.val)
+  merged_id = union!(g.uf, id_1.val, id_2.val)
 
   eclass_2 = pop!(g.classes, id_2)::EClass
   eclass_1 = g.classes[id_1]::EClass
 
-  append!(g.pending, eclass_2.parents)
+  # push!(g.pending, merged_id) 
+  push!(g.pending, id_2.val) # TODO: it seems sufficient to queue parents of id_2.val?
 
   (merged_1, merged_2, new_data) = merge_analysis_data!(eclass_1, eclass_2)
-  merged_1 && append!(g.analysis_pending, eclass_1.parents)
-  merged_2 && append!(g.analysis_pending, eclass_2.parents)
+  merged_1 && push!(g.analysis_pending, id_1.val)
+  merged_2 && push!(g.analysis_pending, id_2.val)
 
 
   # update eclass_1
@@ -380,13 +384,12 @@ function rebuild_classes!(g::EGraph)
     empty!(v)
   end
 
+  trimmed_nodes = 0
   for (eclass_id, eclass) in g.classes
-    # old_len = length(eclass.nodes)
-    for n in eclass.nodes
-      canonicalize!(g, n)
-    end
-    # Sort to go in order?
+    trimmed_nodes += length(eclass.nodes)
+    # TODO Sort to go in order?
     unique!(eclass.nodes)
+    trimmed_nodes -= length(eclass.nodes)
 
     for n in eclass.nodes
       add_class_by_op(g, n, eclass_id.val)
@@ -395,52 +398,129 @@ function rebuild_classes!(g::EGraph)
 
   for v in values(g.classes_by_op)
     sort!(v)
-    unique!(v)
+    unique!(v) # TODO: _groupedunique!(itr), and implement isless(a::VecExpr, b::VecExpr) if it has an performance advantage
   end
+  trimmed_nodes
 end
 
 function process_unions!(g::EGraph{ExpressionType,AnalysisType})::Int where {ExpressionType,AnalysisType}
   n_unions = 0
 
+  # This is close to the pseudo-code in the egg paper.
+  # We separate the worklist into two lists for repair and update of semantic analysis values.
+  # The upwards update of semantic analysis values may require visiting fewer eclasses. 
   while !isempty(g.pending) || !isempty(g.analysis_pending)
-    while !isempty(g.pending)
-      (node::VecExpr, eclass_id::Id) = pop!(g.pending)
-      node = copy(node)
-      canonicalize!(g, node)
-      old_class_id = get!(g.memo, node, eclass_id)
-      if old_class_id != eclass_id
-        did_something = union!(g, old_class_id, eclass_id)
-        # TODO unique! can node dedup be moved here? compare performance
-        # did_something && unique!(g[eclass_id].nodes)
-        n_unions += did_something
+    todo = collect(unique(id -> find(g, id), g.pending))
+    @debug "Worklist reduced from $(length(g.pending)) to $(length(todo)) entries."
+    empty!(g.pending)
+    
+    for id in todo
+      n_unions += repair_parents!(g, id)
+    end
+
+    todo = collect(unique(id -> find(g, id), g.analysis_pending))
+    @debug "Analysis worklist reduced from $(length(g.analysis_pending)) to $(length(todo)) entries."
+    empty!(g.analysis_pending)
+    for id in todo
+      update_analysis_upwards!(g, id)
+    end
+  end
+  n_unions
+end
+
+function repair_parents!(g::EGraph, id::Id)
+  n_unions = 0
+  eclass = g[id] # id does not have to be an eclass id anymore if we merged classes below
+  for (p_node, _) in eclass.parents
+    memo_class = pop!(g.memo, p_node, 0)
+    # memo_class = get(g.memo, p_node, 0)  # TODO: could we be messy instead and just canonicalize the node and add again (without pop!)?
+    
+    # only canonicalize node and update in memo if the node still exists
+    if memo_class > 0
+      canonicalize!(g, p_node)
+      g.memo[p_node] = find(g, memo_class)
+    end
+  end
+
+  # sort and collect unique nodes in new parents list (merging eclasses when finding duplicate nodes) 
+  if !isempty(eclass.parents) 
+    new_parents = Vector{Pair{VecExpr,Id}}()
+    sort!(eclass.parents, by=pair->pair[1])
+    (prev_node, prev_id) = first(eclass.parents)
+    
+    # TODO double check whether we need canonical eclass ids in parents list (find is called in rebuild above anyway)
+    push!(new_parents, prev_node => find(g, prev_id))
+    
+    for i in Iterators.drop(eachindex(eclass.parents), 1)
+      (cur_node, cur_id) = eclass.parents[i]
+      
+      if hash(cur_node) == hash(prev_node) && cur_node == prev_node
+        if union!(g, cur_id, prev_id) 
+          n_unions += 1
+        end
+      else
+        push!(new_parents, cur_node => find(g, cur_id)) # find not necessary?
+        prev_node, prev_id = cur_node, cur_id
       end
     end
+    
+    # TODO: remove assertions
+    # @assert length(unique(pair -> pair[1], new_parents)) == length(new_parents)  "not unique: $new_parents"
+    # @assert all(pair -> pair[2] == find(g, pair[2]), new_parents)  "not refering to eclasses: $(new_parents)\n $g"
+    
+    eclass.parents = new_parents
+  end
+  n_unions
+end
+
+function update_analysis_upwards!(g::EGraph, id::Id)
+  for (p_node, p_id) in g[id].parents
+    p_id = find(g, p_id)
+    eclass = g.classes[IdKey(p_id)]
+
+    node_data = make(g, p_node)
+    if !isnothing(node_data)
+      if !isnothing(eclass.data)
+        joined_data = join(eclass.data, node_data)
 
-    while !isempty(g.analysis_pending)
-      (node::VecExpr, eclass_id::Id) = pop!(g.analysis_pending)
-      eclass_id = find(g, eclass_id)
-      eclass_id_key = IdKey(eclass_id)
-      eclass = g.classes[eclass_id_key]
-
-      node_data = make(g, node)
-      if !isnothing(node_data)
-        if !isnothing(eclass.data)
-          joined_data = join(eclass.data, node_data)
-        
-          if joined_data != eclass.data
-            eclass.data = joined_data
-            modify!(g, eclass)
-            append!(g.analysis_pending, eclass.parents)
-          end
-        else
-          eclass.data = node_data
+        if joined_data != eclass.data
+          eclass.data = joined_data
           modify!(g, eclass)
-          append!(g.analysis_pending, eclass.parents)
+          append!(g.analysis_pending, p_id)
         end
+      else
+        eclass.data = node_data
+        modify!(g, eclass)
+        append!(g.analysis_pending, p_id)
       end
     end
   end
-  n_unions
+end
+
+function check_parents(g::EGraph)::Bool
+  for (id, class) in g.classes
+    # make sure that the parent node and parent eclass occurs in the parents vector for all children
+    for n in class.nodes
+      for chd_id in v_children(n)
+        chd_class = g[chd_id]
+        any(nid -> canonicalize!(g, copy(g.nodes[nid])) == n, chd_class.parents) || error("parent node is missing from child_class.parents")
+        any(nid -> find(g, nid) == id.val, chd_class.parents) || error("missing parent reference from child")
+      end
+    end
+
+    # make sure all nodes and parent ids occuring in the parent vector have this eclass as a child
+    for nid in class.parents
+      parent_class = g[nid]
+      any(n -> any(ch -> ch == id.val, v_children(n)), parent_class.nodes) || error("no node in the parent references the eclass") # nodes are canonicalized
+
+      parent_node = g.nodes[nid]
+      parent_node_copy = copy(parent_node)
+      canonicalize!(g, parent_node_copy)
+      (parent_node_copy in parent_class.nodes) || error("the node from the parent list does not occur in the parent nodes") # might fail because parent_node is probably not canonical
+    end
+  end
+
+  true
 end
 
 function check_memo(g::EGraph)::Bool
@@ -478,9 +558,11 @@ upwards merging in an [`EGraph`](@ref). See
 the [egg paper](https://dl.acm.org/doi/pdf/10.1145/3434304)
 for more details.
 """
-function rebuild!(g::EGraph; should_check_memo=false, should_check_analysis=false)
+function rebuild!(g::EGraph; should_check_parents=false, should_check_memo=false, should_check_analysis=false)
   n_unions = process_unions!(g)
   trimmed_nodes = rebuild_classes!(g)
+
+  @assert !should_check_parents || check_parents(g)
   @assert !should_check_memo || check_memo(g)
   @assert !should_check_analysis || check_analysis(g)
   g.clean = true
diff --git a/src/EGraphs/extract.jl b/src/EGraphs/extract.jl
index 85186b5c..140aba16 100644
--- a/src/EGraphs/extract.jl
+++ b/src/EGraphs/extract.jl
@@ -85,9 +85,9 @@ function find_costs!(extractor::Extractor{CF,CT}) where {CF,CT}
   end
 
   for (id, _) in extractor.g.classes
-    if !haskey(extractor.costs, id)
-      error("failed to compute extraction costs for eclass ", id.val)
-    end
+    # if !haskey(extractor.costs, id)
+    #   error("failed to compute extraction costs for eclass ", id.val)
+    # end
   end
 end
 
diff --git a/src/EGraphs/saturation.jl b/src/EGraphs/saturation.jl
index fcc3555f..59812277 100644
--- a/src/EGraphs/saturation.jl
+++ b/src/EGraphs/saturation.jl
@@ -40,6 +40,8 @@ Base.@kwdef mutable struct SaturationParams
   check_memo::Bool = false
   "Activate check for join-semilattice invariant for semantic analysis values after rebuilding"
   check_analysis::Bool = false
+  "Activate check for parent vectors"
+  check_parents::Bool = false
 end
 
 function cached_ids(g::EGraph, p::PatExpr)::Vector{Id}
@@ -107,7 +109,7 @@ function eqsat_search!(
       # if n_matches - prev_matches > 2 && rule_idx == 2
       #   @debug buffer_readable(g, old_len)
       # end
-      inform!(scheduler, rule_idx, n_matches)
+      inform!(scheduler, rule_idx, n_matches) # TODO - prev_matches
     end
   end
 
@@ -144,14 +146,12 @@ end
 Instantiate argument for dynamic rule application in e-graph
 """
 function instantiate_actual_param!(bindings, g::EGraph, i)
+  const_hash = v_pair_last(bindings[i])
+  const_hash == 0 || return get_constant(g, const_hash)
+
   ecid = v_pair_first(bindings[i])
-  literal_position = reinterpret(Int, v_pair_last(bindings[i]))
   ecid <= 0 && error("unbound pattern variable")
   eclass = g[ecid]
-  if literal_position > 0
-    @assert !v_isexpr(eclass[literal_position])
-    return get_constant(g, v_head(eclass[literal_position]))
-  end
   return eclass
 end
 
@@ -214,7 +214,7 @@ function eqsat_apply!(
     if n_matches % CHECK_GOAL_EVERY_N_MATCHES == 0 && params.goal(g)
       @debug "Goal reached"
       rep.reason = :goalreached
-      return
+      break
     end
 
     delimiter = ematch_buffer.v[k]
@@ -244,24 +244,26 @@ function eqsat_apply!(
 
     res = apply_rule!(bindings, g, rule, id, direction)
 
-    k = next_delimiter_idx
     if res.halt_reason !== :nothing
       rep.reason = res.halt_reason
-      return
+      break
     end
 
+    !iszero(res.l) && !iszero(res.r) && union!(g, res.l, res.r)
+
     if params.enodelimit > 0 && length(g.memo) > params.enodelimit
       @debug "Too many enodes"
       rep.reason = :enodelimit
       break
     end
 
-    !iszero(res.l) && !iszero(res.r) && union!(g, res.l, res.r)
+    k = next_delimiter_idx
+
+    
   end
   if params.goal(g)
     @debug "Goal reached"
     rep.reason = :goalreached
-    return
   end
 
   empty!(ematch_buffer)
@@ -292,10 +294,13 @@ function eqsat_step!(
   if report.reason === nothing && cansaturate(scheduler) && isempty(g.pending)
     report.reason = :saturated
   end
-  @timeit report.to "Rebuild" rebuild!(g; should_check_memo = params.check_memo, should_check_analysis = params.check_analysis)
+ 
+  @timeit report.to "Rebuild" rebuild!(g; 
+    should_check_memo = params.check_memo && report.reason !=:enodelimit, # rules have been applied only partially when the enode limit is reached (TODO)
+    should_check_analysis = params.check_analysis && report.reason !=:enodelimit)
 
   Schedulers.rebuild!(scheduler)
-
+    
   @debug "Smallest expression is" extract!(g, astsize)
 
   return report
@@ -322,7 +327,7 @@ function saturate!(g::EGraph, theory::Theory, params = SaturationParams())
     curr_iter += 1
 
     @debug "================ EQSAT ITERATION $curr_iter  ================"
-    @debug g
+    # @debug g
 
     report = eqsat_step!(g, theory, curr_iter, sched, params, report, ematch_buffer)
 
diff --git a/src/EGraphs/unionfind.jl b/src/EGraphs/unionfind.jl
index f53c0f23..86ef2b20 100644
--- a/src/EGraphs/unionfind.jl
+++ b/src/EGraphs/unionfind.jl
@@ -18,8 +18,10 @@ function Base.union!(uf::UnionFind, i::Id, j::Id)
 end
 
 function find(uf::UnionFind, i::Id)
+  # path splitting
   while i != uf.parents[i]
-    i = uf.parents[i]
+    (i, uf.parents[i]) = (uf.parents[i], uf.parents[uf.parents[i]])
   end
+
   i
 end
diff --git a/src/ematch_compiler.jl b/src/ematch_compiler.jl
index ecb9b5ae..57bc6437 100644
--- a/src/ematch_compiler.jl
+++ b/src/ematch_compiler.jl
@@ -96,12 +96,12 @@ end
 check_constant_exprs!(buf, p::PatLiteral) = push!(buf, :(has_constant(g, $(last(p.n))) || return 0))
 check_constant_exprs!(buf, ::AbstractPat) = buf
 function check_constant_exprs!(buf, p::PatExpr)
-  if !(p.head isa AbstractPat)
-    push!(buf, :(has_constant(g, $(p.head_hash)) || has_constant(g, $(p.quoted_head_hash)) || return 0))
-  end
   for child in children(p)
     check_constant_exprs!(buf, child)
   end
+  if !(p.head isa AbstractPat)
+    push!(buf, :(has_constant(g, $(p.head_hash)) || has_constant(g, $(p.quoted_head_hash)) || return 0))
+  end
   buf
 end
 
@@ -209,8 +209,8 @@ function bind_expr(addr, p::PatExpr, memrange)
       n = eclass.nodes[$(Symbol(:enode_idx, addr))]
 
       v_flags(n) === $(v_flags(p.n)) || @goto $(Symbol(:skip_node, addr))
-      v_signature(n) === $(v_signature(p.n)) || @goto $(Symbol(:skip_node, addr))
-      v_head(n) === $(v_head(p.n)) || (v_head(n) === $(p.quoted_head_hash) || @goto $(Symbol(:skip_node, addr)))
+      v_signature(n) === $(v_signature(p.n)) || @goto $(Symbol(:skip_node, addr)) # TODO better to check signature before flags? check perf.
+      v_head(n) === $(v_head(p.n)) || v_head(n) === $(p.quoted_head_hash) || @goto $(Symbol(:skip_node, addr))
 
       # Node has matched.
       $([:($(Symbol(:σ, j)) = n[$i + $VECEXPR_META_LENGTH]) for (i, j) in enumerate(memrange)]...)
@@ -249,12 +249,12 @@ function check_var_expr(addr, predicate::Function)
   quote
     eclass = g[$(Symbol(:σ, addr))]
     if ($predicate)(g, eclass)
-      for (j, n) in enumerate(eclass.nodes)
-        if !v_isexpr(n)
-          $(Symbol(:enode_idx, addr)) = j + 1
-          break
-        end
-      end
+      # for (j, n) in enumerate(eclass.nodes)
+      #   if !v_isexpr(n)
+      #     $(Symbol(:enode_idx, addr)) = j + 1
+      #     break
+      #   end
+      # end
       pc += 0x0001
       @goto compute
     end
@@ -322,7 +322,17 @@ end
 
 function yield_expr(patvar_to_addr, direction)
   push_exprs = [
-    :(push!(ematch_buffer, v_pair($(Symbol(:σ, addr)), reinterpret(UInt64, $(Symbol(:enode_idx, addr)) - 1)))) for
+    quote
+      id = $(Symbol(:σ, addr))
+      eclass = g[id]
+      node_idx = $(Symbol(:enode_idx, addr)) - 1
+      if node_idx <= 0
+        push!(ematch_buffer, v_pair(id, reinterpret(UInt64, 0)))
+      else
+        n = eclass.nodes[node_idx]
+        push!(ematch_buffer, v_pair(id, v_head(n)))
+      end
+    end for
     addr in patvar_to_addr
   ]
   quote
diff --git a/src/optbuffer.jl b/src/optbuffer.jl
index 94a1d3f6..82a183b3 100644
--- a/src/optbuffer.jl
+++ b/src/optbuffer.jl
@@ -34,4 +34,4 @@ end
 Base.isempty(b::OptBuffer{T}) where {T} = b.i === 0
 Base.empty!(b::OptBuffer{T}) where {T} = (b.i = 0)
 @inline Base.length(b::OptBuffer{T}) where {T} = b.i
-Base.iterate(b::OptBuffer{T}, i=1) where {T} = iterate(b.v[1:b.i], i)
\ No newline at end of file
+Base.iterate(b::OptBuffer{T}, i=1) where {T} = i <= b.i ? (b.v[i], i + 1) : nothing
\ No newline at end of file
diff --git a/src/vecexpr.jl b/src/vecexpr.jl
index c18059f9..eee3a7eb 100644
--- a/src/vecexpr.jl
+++ b/src/vecexpr.jl
@@ -121,4 +121,6 @@ v_pair_last(p::UInt128)::UInt64 = UInt64(p & 0xffffffffffffffff)
 @inline Base.lastindex(n::VecExpr) = lastindex(n.data)
 @inline Base.firstindex(n::VecExpr) = firstindex(n.data)
 
+Base.isless(a::VecExpr,b::VecExpr) = isless(a.data,b.data)
+
 end
diff --git a/test/egraphs/egraphs.jl b/test/egraphs/egraphs.jl
index 4bc4b51e..b600fb40 100644
--- a/test/egraphs/egraphs.jl
+++ b/test/egraphs/egraphs.jl
@@ -4,10 +4,29 @@ using Test, Metatheory
 @testset "Merging" begin
   testexpr = :((a * 2) / 2)
   testmatch = :(a << 1)
-  g = EGraph(testexpr)
+  g = EGraph()
+  testexpr_id = addexpr!(g, testexpr)
+  t1 = addexpr!(g, :(a * 2)) # get eclass id of a * 2
+  t1_node = copy(g[t1].nodes[1])
+  
   t2 = addexpr!(g, testmatch)
-  union!(g, t2, Id(3))
-  @test find(g, t2) == find(g, Id(3))
+  t2_node = copy(g[t2].nodes[1])
+  union!(g, t2, t1)
+
+  @testset "Behaviour" begin
+    @test find(g, t2) == find(g, t1)
+  end
+
+  @testset "Internals" begin
+    @test length(g[t1].nodes) == 2 # a << 1, a * 2
+    @test g[t1].parents == [g[testexpr_id].nodes[1] => testexpr_id]
+
+    # the parents of child eclasses are only touched when we need them (upwards repair only)
+    # id_1 = addexpr!(g, 1) # get id of constant 1
+    # @test g[id_1].parents == [t1_node => find(g, t1)] # just eclass [a << 1, a * 2]
+    # id_a = addexpr!(g, :a)
+    # @test g[id_a].parents == [t2_node => find(g, t1)] # just eclass [a << 1, a * 2]
+  end
 end
 
 # testexpr = :(42a + b * (foo($(Dict(:x => 2)), 42)))
@@ -25,10 +44,21 @@ end
   t2 = addexpr!(g, :c)
 
   union!(g, t2, t1)
-  @test find(g, t2) == find(g, t1)
-  @test find(g, t2) == find(g, t1)
-  rebuild!(g)
-  @test find(g, ec1) == find(g, ec2)
+  @testset "Behaviour" begin
+    @test find(g, t2) == find(g, t1)
+    rebuild!(g)
+    @test find(g, ec1) == find(g, ec2)
+    @test length(g[ec2].nodes) == 1
+  end
+
+  @testset "Internals" begin
+    aid = addexpr!(g, :a) # get id of :a
+    @assert length(g[ec2].nodes) == 1
+    # @test g[aid].parents == [g[ec1].nodes[1] => find(g, ec1)]
+    # @test g[t1].parents == [g[ec1].nodes[1] => find(g, ec1)]
+    @test length(g[testec].nodes) == 1
+    @test g[ec1].parents == [g[testec].nodes[1] => find(g, testec)]
+  end
 end
 
 
@@ -43,29 +73,37 @@ end
   t1 = addexpr!(g, apply(6, f, :a))
   t2 = addexpr!(g, apply(9, f, :a))
 
-  c_id = union!(g, t1, a) # a == apply(6,f,a)
-  c2_id = union!(g, t2, a) # a == apply(9,f,a)
+  union!(g, t1, a) # a == apply(6,f,a)
+  union!(g, t2, a) # a == apply(9,f,a)
 
   rebuild!(g)
 
-  pretty_dict(g)
-
   t3 = addexpr!(g, apply(3, f, :a))
   t4 = addexpr!(g, apply(7, f, :a))
 
-  # f^m(a) = a = f^n(a) ⟹ f^(gcd(m,n))(a) = a
-  @test find(g, t1) == find(g, a)
-  @test find(g, t2) == find(g, a)
-  @test find(g, t3) == find(g, a)
-  @test find(g, t4) != find(g, a)
-
-  # if m or n is prime, f(a) = a
-  t5 = addexpr!(g, apply(11, f, :a))
-  t6 = addexpr!(g, apply(1, f, :a))
-  c5_id = union!(g, t5, a) # a == apply(11,f,a)
-
-  rebuild!(g)
-
-  @test find(g, t5) == find(g, a)
-  @test find(g, t6) == find(g, a)
+  t6_node = 0
+  t5 = 0
+  @testset "Behaviour" begin
+    # f^m(a) = a = f^n(a) ⟹ f^(gcd(m,n))(a) = a
+    @test find(g, t1) == find(g, a)
+    @test find(g, t2) == find(g, a)
+    @test find(g, t3) == find(g, a)
+    @test find(g, t4) != find(g, a)
+
+    # if m or n is prime, f(a) = a
+    t5 = addexpr!(g, apply(11, f, :a))
+    t6 = addexpr!(g, apply(1, f, :a))
+    t6_node = g[t6].nodes[1]
+    union!(g, t5, a) # a == apply(11,f,a)
+
+    rebuild!(g)
+
+    @test find(g, t5) == find(g, a)
+    @test find(g, t6) == find(g, a)
+  end
+
+  @testset "Internals" begin
+    @test length(g.classes) == 1 # only a single class %id [:a, f(%id)] remains
+    @test length(g[a].parents) == 1 # there can be only a single parent
+  end
 end
diff --git a/test/integration/cas.jl b/test/integration/cas.jl
index 5fd1c068..6e8ac197 100644
--- a/test/integration/cas.jl
+++ b/test/integration/cas.jl
@@ -1,4 +1,4 @@
-using Metatheory, TermInterface, Test
+using Metatheory, Test
 using Metatheory.Library
 using Metatheory.Schedulers
 
@@ -145,14 +145,14 @@ function simplcost(n::VecExpr, op, costs)
   1 + sum(costs) + (op in (:∂, diff, :diff) ? 200 : 0)
 end
 
-function simplify(ex; steps = 4)
-  params = SaturationParams(
+function simplify(ex; steps = 4, params=SaturationParams())
+  #params = SaturationParams(
   # scheduler = ScoredScheduler,
   # eclasslimit = 5000,
-  # timeout = 7,
+  # timeout = 2,
   # schedulerparams = (match_limit = 1000, ban_length = 5),
   #stopwhen=stopwhen,
-  )
+  #)
   hist = UInt64[]
   push!(hist, hash(ex))
   for i in 1:steps
diff --git a/test/tutorials/lambda_theory.jl b/test/tutorials/lambda_theory.jl
index 9f74a725..1219d385 100644
--- a/test/tutorials/lambda_theory.jl
+++ b/test/tutorials/lambda_theory.jl
@@ -1,4 +1,4 @@
-using Metatheory, Test, TermInterface
+using Metatheory, Test
 
 # # Lambda theory
 #