diff --git a/src/buffer_pair.jl b/src/buffer_pair.jl
index a6dc9584..0e0628e1 100644
--- a/src/buffer_pair.jl
+++ b/src/buffer_pair.jl
@@ -2,37 +2,34 @@ struct RewritingBuffer{T,V<:AbstractVector}
     output::Words.BufferWord{T}
     input::Words.BufferWord{T}
     history::V
+
+    function RewritingBuffer{T}(
+        output::BW,
+        input::BW,
+        history::AbstractVector,
+    ) where {T,BW<:Words.BufferWord{T}}
+        return new{T,typeof(history)}(output, input, history)
+    end
+
+    function RewritingBuffer{T}(
+        output::BW,
+        input::BW,
+    ) where {T,BW<:Words.BufferWord{T}}
+        return new{T,Vector{Int}}(output, input)
+    end
+end
+
+function RewritingBuffer{T}() where {T}
+    BW = Words.BufferWord{T}
+    return RewritingBuffer{T}(one(BW), one(BW))
 end
 
 function RewritingBuffer{T}(history::AbstractVector) where {T}
     BW = Words.BufferWord{T}
-    return RewritingBuffer(one(BW), one(BW), history)
+    return RewritingBuffer{T}(one(BW), one(BW), history)
 end
 
 function Words.store!(rwbuf::RewritingBuffer, u::AbstractWord...)
     Words.store!(rwbuf.input, u...)
     return rwbuf
 end
-
-"""
-    function rewrite!(bp::BufferPair, rewriting; kwargs...)
-Rewrites word stored in `BufferPair` using `rewriting` object.
-
-To store a word in `bp`
-[`Words.store!`](@ref Words.store!(::BufferPair, ::AbstractWord))
-should be used.
-
-!!! warning
-    This implementation returns an instance of `Words.BufferWord` aliased with
-    the intenrals of `BufferPair`. You need to copy the return value if you
-    want to take the ownership.
-"""
-function rewrite!(bp::RewritingBuffer, rewriting; kwargs...)
-    v = if isempty(rewriting)
-        Words.store!(bp.output, bp.input)
-    else
-        rewrite!(bp.output, bp.input, rewriting; history = bp.history, kwargs...)
-    end
-    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
-    return v
-end
diff --git a/src/knuthbendix2.jl b/src/knuthbendix2.jl
index e8f62726..d0f3b220 100644
--- a/src/knuthbendix2.jl
+++ b/src/knuthbendix2.jl
@@ -65,7 +65,10 @@ function find_critical_pairs!(
     lhs₁, rhs₁ = r₁
     lhs₂, rhs₂ = r₂
     m = min(length(lhs₁), length(lhs₂)) - 1
-    W = word_type(stack)
+    if m > work.settings.max_length_overlap
+        m = work.settings.max_length_overlap
+        work.dropped_rules += 1
+    end
 
     # TODO: cache suffix automaton for lhs₁ to run this in O(m) (currently: O(m²))
     for b in suffixes(lhs₁, 1:m)
@@ -104,9 +107,13 @@ function deriverule!(
         u, v = pop!(stack)
         critical, (a, b) = _iscritical(work, rws, (u,), (v,))
         if critical
-            new_rule = Rule{W}(a => b)
-            push!(rws, new_rule)
-            deactivate_rules!(rws, stack, new_rule, work)
+            if isadmissible(a, b, work.settings)
+                new_rule = Rule{W}(a => b)
+                push!(rws, new_rule)
+                deactivate_rules!(rws, stack, new_rule, work)
+            else
+                work.dropped_rules += 1
+            end
         end
     end
 end
diff --git a/src/knuthbendix_base.jl b/src/knuthbendix_base.jl
index c6102efa..22c64938 100644
--- a/src/knuthbendix_base.jl
+++ b/src/knuthbendix_base.jl
@@ -51,20 +51,14 @@ function knuthbendix(
         finish!(prog)
 
         if isreduced(rws_dc)
-            if !isconfluent(rws_dc) # sets the confluence flag
-                if settings.verbosity > 0
-                    @warn "The returned rws is not confluent"
-                end
-            end
-        else
-            if settings.verbosity > 0
-                @warn "the returned rws is not reduced"
+            confluent = isconfluent(rws_dc) # sets the confluence flag
+            if !confluent && settings.verbosity > 0
+                @warn "The returned rws is not confluent"
             end
         end
         return rws_dc
     catch e
         if e isa InterruptException
-            rethrow(e)
             @warn """Received user interrupt in Knuth-Bendix completion.
             Returned rws may be not confluent."""
             @info """Attempting to reduce the rewriting system.
diff --git a/src/knuthbendix_idxA.jl b/src/knuthbendix_idxA.jl
index 6f23442e..c96110d9 100644
--- a/src/knuthbendix_idxA.jl
+++ b/src/knuthbendix_idxA.jl
@@ -75,7 +75,10 @@ function knuthbendix!(
             end
             @assert isempty(stack)
             stack, i_after = check_confluence!(stack, rws, idxA, work)
-            isempty(stack) && return rws # yey, we're done!
+            if isempty(stack)
+                __post!(rws, idxA, work)
+                return rws # yey, we're done!
+            end
             if settings.verbosity == 2
                 l = length(stack)
                 @info "confluence check failed: found $(l) new rule$(l==1 ? "" : "s")"
@@ -129,5 +132,40 @@ function knuthbendix!(
         end
         i += 1
     end
+
+    __post!(rws, idxA, work)
+
     return rws # so the rws is reduced here as well
 end
+
+function __post!(rws::AbstractRewritingSystem, rewriting, work::Workspace)
+    settings = work.settings
+    stack = Vector{Tuple{word_type(rws),word_type(rws)}}()
+
+    if work.dropped_rules > 0
+        @assert isempty(stack)
+        if settings.verbosity ≥ 2
+            @info "KnuthBendix completion has finished, however some rules were dropped; re-adding the defining rules"
+        end
+        for (lhs, rhs) in rws.rules_orig
+            Words.store!(work.rewrite1, lhs)
+            l = rewrite!(work.rewrite1, rewriting)
+            Words.store!(work.rewrite2, rhs)
+            r = rewrite!(work.rewrite2, rewriting)
+            if l ≠ r
+                push!(stack, (l, r))
+            end
+        end
+        if !isempty(stack)
+            if settings.verbosity ≥ 1
+                @warn "The rws does NOT represent the original congruence. Re-adding the missing rules."
+            end
+            rws = reduce!(settings.algorithm, rws, stack, work)
+        else
+            if settings.verbosity == 2
+                @info "Some rules have been dropped but the congruence is preserved."
+            end
+        end
+    end
+    return rws
+end
diff --git a/src/parsing.jl b/src/parsing.jl
index 1bd24180..77516f9d 100644
--- a/src/parsing.jl
+++ b/src/parsing.jl
@@ -26,6 +26,7 @@ struct KbmagRWS
     inverses::Vector{Int}
     equations::Vector{Pair{Vector{Int},Vector{Int}}}
     ordering::String
+    options::Dict{Symbol,Int}
     _str::String
 end
 
@@ -41,7 +42,7 @@ function Base.show(io::IO, ::MIME"text/plain", rws::KbmagRWS)
     println(io, ']', ',')
 
     print(io, lpad(:inverses, padlen), " := [")
-    join(io, rws.generatorOrder[rws.inverses], ',')
+    join(io, (i > 0 ? rws.generatorOrder[i] : ' ' for i in rws.inverses), ',')
     println(io, ']', ',')
 
     println(io, lpad(:ordering, padlen), " := \"", rws.ordering, "\"", ',')
@@ -188,6 +189,39 @@ function _parse_ordering(str::AbstractString)
     return strip(m[:ordering])
 end
 
+function _parse_opts(str::AbstractString)
+    options = Dict{Symbol,Int}()
+    r = _entry_regex(
+        "maxstoredlen",
+        "\\[\\s*(?<lhs_len>\\d+)\\s*,\\s*(?<rhs_len>\\d+)\\s*\\]",
+    )
+    m = match(r, str)
+    if !isnothing(m)
+        options[:max_length_lhs] = parse(Int, m[:lhs_len])
+        options[:max_length_rhs] = parse(Int, m[:rhs_len])
+    end
+
+    r = _entry_regex("tidyint", "(?<tidyint>\\d+)")
+    m = match(r, str)
+    if !isnothing(m)
+        options[:stack_size] = parse(Int, m[:tidyint])
+    end
+
+    r = _entry_regex("maxeqns", "(?<maxeqns>\\d+)")
+    m = match(r, str)
+    if !isnothing(m)
+        options[:max_rules] = parse(Int, m[:maxeqns])
+    end
+
+    r = _entry_regex("maxstates", "(?<maxstates>\\d+)")
+    m = match(r, str)
+    if !isnothing(m)
+        options[:max_states] = parse(Int, m[:maxstates])
+    end
+
+    return options
+end
+
 function parse_kbmag(input::AbstractString)
     rws_str = _validate_rws(input)
 
@@ -202,7 +236,16 @@ function parse_kbmag(input::AbstractString)
     end
     ordering = _parse_ordering(rws_str)
 
-    return KbmagRWS(Symbol.(gens), inverses, equations, ordering, rws_str)
+    options = _parse_opts(rws_str)
+
+    return KbmagRWS(
+        Symbol.(gens),
+        inverses,
+        equations,
+        ordering,
+        options,
+        rws_str,
+    )
 end
 
 RewritingSystem(rwsgap::KbmagRWS) = RewritingSystem{Word{UInt16}}(rwsgap)
@@ -221,3 +264,13 @@ function RewritingSystem{W}(rwsgap::KbmagRWS) where {W}
 
     return RewritingSystem(rwrules, ordering)
 end
+
+function Settings(rwsgap::KbmagRWS)
+    return Settings(
+        KBIndex();
+        (
+            opt for
+            opt in pairs(rwsgap.options) if first(opt) in fieldnames(Settings)
+        )...,
+    )
+end
diff --git a/src/rewriting.jl b/src/rewriting.jl
index aae4b819..b1c9bb10 100644
--- a/src/rewriting.jl
+++ b/src/rewriting.jl
@@ -1,3 +1,6 @@
+RewritingBuffer{T}(::Any) where {T} = RewritingBuffer{T}() # no history
+RewritingBuffer{T}(::IndexAutomaton{S}) where {T,S} = RewritingBuffer{T}(S[])
+
 """
     rewrite(u::AbstractWord, rewriting)
 Rewrites word `u` using the `rewriting` object. The object must implement
@@ -27,15 +30,13 @@ true
 function rewrite(
     u::W,
     rewriting,
-    vbuff = Words.BufferWord{T}(0, length(u)),
-    wbuff = Words.BufferWord{T}(0, length(u));
+    rwbuffer::RewritingBuffer = RewritingBuffer{T}(rewriting);
     kwargs...,
 ) where {T,W<:AbstractWord{T}}
-    isempty(rewriting) && return W(u, false)
-    Words.store!(wbuff, u)
-    v = rewrite!(vbuff, wbuff, rewriting; kwargs...)
-    res = W(v, false)
-    return res
+    isempty(rewriting) && return W(u)
+    Words.store!(rwbuffer, u)
+    v = rewrite!(rwbuffer, rewriting; kwargs...)
+    return W(v)
 end
 
 function rewrite!(v::AbstractWord, w::AbstractWord, A::Any; kwargs...)
@@ -149,7 +150,7 @@ See procedure `REWRITE_FROM_LEFT` from **Section 2.4**[^Sims1994], p. 66.
 function rewrite!(
     v::AbstractWord,
     w::AbstractWord,
-    rws::RewritingSystem;
+    rws::AbstractRewritingSystem;
     kwargs...,
 )
     v = empty!(v)
@@ -230,3 +231,35 @@ function rewrite!(
     end
     return v
 end
+
+"""
+    function rewrite!(bp::BufferPair, rewriting; kwargs...)
+Rewrites word stored in `BufferPair` using `rewriting` object.
+
+To store a word in `bp`
+[`Words.store!`](@ref Words.store!(::BufferPair, ::AbstractWord))
+should be used.
+
+!!! warning
+    This implementation returns an instance of `Words.BufferWord` aliased with
+    the intenrals of `BufferPair`. You need to copy the return value if you
+    want to take the ownership.
+"""
+function rewrite!(bp::RewritingBuffer, rewriting; kwargs...)
+    v = if isempty(rewriting)
+        Words.store!(bp.output, bp.input)
+    else
+        rewrite!(bp.output, bp.input, rewriting; kwargs...)
+    end
+    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
+    return v
+end
+function rewrite!(bp::RewritingBuffer, rewriting::IndexAutomaton; kwargs...)
+    v = if isempty(rewriting)
+        Words.store!(bp.output, bp.input)
+    else
+        rewrite!(bp.output, bp.input, rewriting; history = bp.history, kwargs...)
+    end
+    empty!(bp.input) # shifts bp._wWord pointers to the beginning of its storage
+    return v
+end
diff --git a/src/settings_workspace.jl b/src/settings_workspace.jl
index 943f0f13..6f56b3d9 100644
--- a/src/settings_workspace.jl
+++ b/src/settings_workspace.jl
@@ -33,7 +33,6 @@ mutable struct Settings{CA<:CompletionAlgorithm}
     max_length_rhs::Int
     max_length_overlap::Int
     verbosity::Int
-    dropped_rules::Bool
     update_progress::Any
 
     function Settings(
@@ -41,9 +40,9 @@ mutable struct Settings{CA<:CompletionAlgorithm}
         max_rules = 10000,
         stack_size = 100,
         confluence_delay = 10,
-        max_length_lhs = 100,
-        max_length_rhs = 1000,
-        max_length_overlap = 0,
+        max_length_lhs = typemax(Int),
+        max_length_rhs = typemax(Int),
+        max_length_overlap = typemax(Int),
         verbosity = 0,
     )
         return new{typeof(alg)}(
@@ -55,7 +54,6 @@ mutable struct Settings{CA<:CompletionAlgorithm}
             max_length_rhs,
             max_length_overlap,
             verbosity,
-            false,
             (args...) -> nothing,
         )
     end
@@ -77,22 +75,12 @@ function isadmissible(lhs, rhs, s::Settings)
     return length(lhs) ≤ s.max_length_lhs && length(rhs) ≤ s.max_length_rhs
 end
 
-function Base.filter!(sett::Settings, stack::AbstractVector)
-    to_delete = falses(length(stack))
-    for i in eachindex(stack)
-        to_delete[i] = !isadmissible(stack[i]..., sett)
-    end
-    if any(to_delete)
-        deleteat!(stack, to_delete)
-    end
-    return stack
-end
-
 mutable struct Workspace{CA,T,H,S<:Settings{CA}}
     rewrite1::RewritingBuffer{T,H}
     rewrite2::RewritingBuffer{T,H}
     settings::S
     confluence_timer::Int
+    dropped_rules::Int
 end
 
 function Workspace(word_t, history, settings::Settings)
@@ -102,6 +90,7 @@ function Workspace(word_t, history, settings::Settings)
         BP_t(deepcopy(history)),
         settings,
         0,
+        0,
     )
 end
 
diff --git a/test/automata.jl b/test/automata.jl
index 4435998e..c71cbeb5 100644
--- a/test/automata.jl
+++ b/test/automata.jl
@@ -1,5 +1,3 @@
-import KnuthBendix.Automata
-
 @testset "States" begin
     S = Automata.State{Symbol,UInt32,String}
     @test S() isa Automata.State
diff --git a/test/gapdoc_examples.jl b/test/gapdoc_examples.jl
index 5f0bc663..b736e2b0 100644
--- a/test/gapdoc_examples.jl
+++ b/test/gapdoc_examples.jl
@@ -108,27 +108,7 @@
 
         rws = KnuthBendix.RewritingSystem(rels, KnuthBendix.Recursive(alph))
 
-        R = let R = rws
-            for _ in 1:10
-                R = @time knuthbendix(sett, R)
-                # this is hacking, todo: implement using Settings.max_length_lhs
-                after_kbc = KnuthBendix.nrules(R)
-                filter!(r -> KB.isadmissible(r..., sett), R.rwrules)
-                after_flt = KnuthBendix.nrules(R)
-                append!(R.rwrules, R.rules_orig)
-                R.reduced = false
-                R.confluent = false
-                KnuthBendix.reduce!(R)
-                append_org = KnuthBendix.nrules(R)
-                @info "number of rules" after_kbc after_flt append_org
-                isempty(KB.check_confluence(R)) && break
-            end
-            R
-        end
-
-        # replace the above by this
-        # after the filtering of rules is implemented in knuthbendix
-        # R = knuthbendix(sett, rws)
+        R = knuthbendix(sett, rws)
 
         @test KB.isreduced(R)
         @test KB.isconfluent(R)
diff --git a/test/kbmag_parsing.jl b/test/kbmag_parsing.jl
index 781a294c..bea48e57 100644
--- a/test/kbmag_parsing.jl
+++ b/test/kbmag_parsing.jl
@@ -46,11 +46,42 @@ using MacroTools
                      )"""
             @test sprint(show, MIME"text/plain"(), rws) == res
         end
+        let file_content = String(read(joinpath(kb_data, "cosets")))
+            rws = KnuthBendix.parse_kbmag(file_content)
+            @test rws.generatorOrder == [:H, :a, :A, :b, :B]
+            @test rws.inverses == [0, 3, 2, 5, 4]
+            @test rws.equations == [
+                [2, 2, 2] => Int[],
+                [4, 4, 4, 4] => Int[],
+                [2, 4, 2, 4] => Int[],
+                [1, 4] => [1],
+                [1, 1] => [1],
+                [2, 1] => [1],
+                [4, 1] => [1],
+            ]
+
+            res = """rec(
+                                isRWS := true,
+                       generatorOrder := [H,a,A,b,B],
+                             inverses := [ ,A,a,B,b],
+                             ordering := "shortlex",
+                            equations := [
+                         [a*a*a, IdWord],
+                         [b*b*b*b, IdWord],
+                         [a*b*a*b, IdWord],
+                         [H*b, H],
+                         [H*H, H],
+                         [a*H, H],
+                         [b*H, H]
+                       ]
+                     )"""
+            @test sprint(show, MIME"text/plain"(), rws) == res
+        end
     end
 
     failed_exs = [
         # times with `stack_size = 250`
-        "degen4b",    # too hard
+        # "degen4b",    # < 0.1s with max_length_lhs = 20
         "degen4c",    # too hard
         # "237_8",    #   1.885474 seconds (106.73 k allocations: 11.966 MiB)
         # "e8",       #   2.146169 seconds (106.69 k allocations: 10.614 MiB)
@@ -61,7 +92,7 @@ using MacroTools
         "heinnilp",   #  77.018298 seconds (476.10 k allocations: 77.103 MiB)
         # "l32ext",   #   2.267469 seconds (115.22 k allocations: 13.604 MiB)
         # "m11", # 37.746448 seconds (311.76 k allocations: 59.166 MiB, 0.06% gc time)
-        "verifynilp", # too hard
+        # "verifynilp", # too hard
     ]
 
     @testset "kbmag example: $fn" for fn in readdir(kb_data)
@@ -75,14 +106,12 @@ using MacroTools
         end
         @test RewritingSystem(rwsgap) isa RewritingSystem
 
-        sett = KnuthBendix.Settings(
-            KB.KBIndex(),
-            max_rules = 25_000,
-            verbosity = 0,
-            stack_size = 100,
-        )
+        sett = KB.Settings(rwsgap)
+        if fn == "degen4b"
+            sett.max_length_lhs = 20
+        end
         fn in failed_exs && continue
-        @info fn
+        @info fn # sett
         rws = RewritingSystem(rwsgap)
         @time R = knuthbendix(sett, rws)
         @test isconfluent(R)
diff --git a/test/runtests.jl b/test/runtests.jl
index ec998aa0..59bc25b6 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -2,6 +2,7 @@ using KnuthBendix
 using Test
 using Documenter
 import KnuthBendix as KB
+import KnuthBendix.Automata
 
 include("abstract_words.jl")