diff --git a/src/rewrite/Constraints.jl b/src/rewrite/Constraints.jl
index ecd247c..6c5deaa 100644
--- a/src/rewrite/Constraints.jl
+++ b/src/rewrite/Constraints.jl
@@ -190,12 +190,12 @@ function Base.show(io::IO, c::Quantifier)
 end
 subexprs(q::Quantifier) = [q.expr, q.st]
 
-Exists!(e,x;st=True,monic=false) = Quantifier(e,:Exists,x;st=st,monic=monic)
-Forall(e,x;st=True,monic=false) = Quantifier(e,:Forall,x;st=st,monic=monic)
-Exists(e,x;st=True,monic=false) = Quantifier(e,:Exists,x;st=st,monic=monic)
-∀(args...;kwargs...) = Forall(args...;kwargs...)
-∃(args...;kwargs...) = Exists(args...;kwargs...)
-∃!(args...;kwargs...) = Exists!(args...;kwargs...)
+Exists!(e,x; st=True, monic=false) = Quantifier(e,:Exists,x; st, monic)
+Forall(e, x; st=True, monic=false) = Quantifier(e,:Forall,x; st, monic)
+Exists(e, x; st=True, monic=false) = Quantifier(e,:Exists,x; st, monic)
+∀(args...; kwargs...) = Forall(args...; kwargs...)
+∃(args...; kwargs...) = Exists(args...; kwargs...)
+∃!(args...; kwargs...) = Exists!(args...; kwargs...)
 
 """Disjunction of multiple expressions"""
 @struct_hash_equal struct BoolOr <: BoolExpr 
@@ -290,7 +290,8 @@ function eval_boolexpr(q::Quantifier, g::CGraph, curr::Assgn)
   d, cd = [get_ob(g,x,curr) for x in [g[q.e, :src], g[q.e, :tgt]]]
   cands = []
   @debug "$(q.kind) ($(q.e))"
-  for h in homomorphisms(d, cd; monic=q.monic)
+  monic = q.monic == true ? ob(acset_schema(d)) : q.monic
+  for h in homomorphisms(d, cd; monic)
     x = deepcopy(curr)
     x[q.e] = h 
     @debug "candidate morphism $(components(h))"
diff --git a/src/rewrite/PBPO.jl b/src/rewrite/PBPO.jl
index 75790c1..d01ffa9 100644
--- a/src/rewrite/PBPO.jl
+++ b/src/rewrite/PBPO.jl
@@ -132,7 +132,7 @@ function get_matches(rule::PBPORule, G::ACSet;  initial=nothing,
 
   # Search for each match morphism
   backtracking_search(L, G; monic=rule.monic, initial=NamedTuple(matchinit),
-                      random=random) do m
+                      random) do m
     m_seen = false # keeps track if α_unique is violated for each new m
     if all(ac->apply_constraint(ac, m), rule.acs)
       @debug "m:  $([k=>collect(v) for (k,v) in pairs(components(m))])"
diff --git a/src/rewrite/Utils.jl b/src/rewrite/Utils.jl
index c9e64d4..bfec796 100644
--- a/src/rewrite/Utils.jl
+++ b/src/rewrite/Utils.jl
@@ -61,7 +61,7 @@ condition(s)
     else 
       exprs = Dict(map(attrtypes(acset_schema(dom(L)))) do o
         binding = Dict()
-        for r_var in parts(codom(R),o)
+        for r_var in parts(codom(R), o)
           # User explicitly provides a function to evaluate for this variable
           if !isnothing(expr) && haskey(expr, o) && r_var ∈ keys(expr[o])
             binding[r_var] = expr[o][r_var]
@@ -112,7 +112,7 @@ get_result(sem::Symbol, maps) = codom(get_rmap(sem, maps))
 """Extract the partial map (derived rule) from full output data"""
 function get_pmap(sem::Symbol, maps)
   if isnothing(maps)  nothing
-  elseif sem ∈ DPO′  Span(maps[:kg], maps[:kh])
+  elseif sem ∈ DPO′   Span(maps[:kg], maps[:kh])
   elseif sem == :SPO  Span(maps[:gmono], maps[:gmap])
   elseif sem == :SqPO Span(maps[:i], maps[:o])
   elseif sem == :PBPO Span(maps[:gl], maps[:gr])
@@ -125,10 +125,10 @@ end
 check_initial(vs::Vector{Int}, f::Vector{Int}) =
   [(i, vs[i], f[i]) for i in length(f) if vs[i]!=f[i]]
 check_initial(vs::Vector{Pair{Int,Int}}, f::Vector{Int}) =
-  [(i,f[i],v) for (i,v) in vs if f[i]!=v]
+  [(i, f[i], v) for (i, v) in vs if f[i]!=v]
 
 # Check if a component is included in a monic constraint
-has_comp(monic::Bool, c::Symbol) = monic
+has_comp(monic::Bool, ::Symbol) = monic
 has_comp(monic::Vector{Symbol}, c::Symbol) = c ∈ monic
 
 """
@@ -138,14 +138,14 @@ rule, otherwise returns the reason why it should be rejected
 function can_match(r::Rule{T}, m; initial=Dict()) where T
   S = acset_schema(dom(m))
   for k in ob(S)
-    if has_comp(r.monic,k) && !is_monic(m[k])
+    if has_comp(r.monic, k) && !is_monic(m[k])
       return ("Match is not injective", k, m[k])
     end
   end
   for (k, vs) in collect(initial)
     errs = check_initial(vs, collect(m[k]))
     if !isempty(errs)
-      return ("Initial condition violated",k, errs)
+      return ("Initial condition violated", k, errs)
     end
   end
 
@@ -183,8 +183,8 @@ function get_matches(r::Rule{T}, G::ACSet; initial=nothing,
 
   hs = []
   backtracking_search(codom(r.L), G; monic=r.monic, initial=NamedTuple(initial), 
-                      random=random) do h 
-    cm = can_match(r,h)
+                      random) do h 
+    cm = can_match(r, h)
     if isnothing(cm)
       push!(hs, deepcopy(h))
       return length(hs) == n # we stop the search Hom(L,G) when this holds
@@ -200,7 +200,7 @@ end
 function get_matches(r::Rule{T}, G; initial=nothing, random=false, n=-1) where T 
   initial = isnothing(initial) ? Dict() : initial
   ms = homomorphisms(codom(left(r)), G; monic=r.monic, 
-                     initial=NamedTuple(initial), random=random)
+                     initial=NamedTuple(initial), random)
   res = []
   for m in ms 
     if (n < 0 || length(res) < n) && isnothing(can_match(r, m))
@@ -258,7 +258,7 @@ function rewrite_match_maps end  # to be implemented for each T
 Perform a rewrite (automatically finding an arbitrary match) and return result.
 """
 function rewrite(r::AbsRule, G; initial=nothing, random=false, kw...)
-  m = get_match(r, G; initial=initial, random=random)
+  m = get_match(r, G; initial=initial, random)
   return isnothing(m) ? nothing : rewrite_match(r, m; kw...)
 end
 
@@ -279,7 +279,7 @@ Perform a rewrite (automatically finding an arbitrary match) and return a tuple:
 function rewrite_full_output(r::AbsRule, G; initial=nothing, random=false,
                              n=-1, kw...) 
   T = ruletype(r)
-  ms = get_matches(r,G,initial=initial, random=random, n=n)
+  ms = get_matches(r, G; initial, random, n)
   if isempty(ms)
     return nothing
   elseif random