diff --git a/test/issue-3508/definition.kore b/test/issue-3508/definition.kore
index d6aa2c1c3a..a771572b76 100644
--- a/test/issue-3508/definition.kore
+++ b/test/issue-3508/definition.kore
@@ -228,7 +228,7 @@ module IMP
   hooked-symbol Lbl'Hash'open'LParUndsCommUndsRParUnds'K-IO'Unds'IOInt'Unds'String'Unds'String{}(SortString{}, SortString{}) : SortIOInt{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), impure{}(), hook{}("IO.open"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2408,18,2408,97)"), left{}(), format{}("%c#open%r %c(%r %1 %c,%r %2 %c)%r"), function{}()]
   symbol Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(SortInt{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#ostream"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2589,21,2589,34)"), left{}(), format{}("%c#ostream%r %c(%r %1 %c)%r"), injective{}()]
   symbol Lbl'Hash'parseInput'LParUndsCommUndsRParUnds'K-IO'Unds'Stream'Unds'String'Unds'String{}(SortString{}, SortString{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), klabel{}("#parseInput"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2588,21,2588,48)"), left{}(), format{}("%c#parseInput%r %c(%r %1 %c,%r %2 %c)%r"), injective{}()]
-  hooked-symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), hook{}("KREFLECTION.parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2265,26,2265,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}()]
+  symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2265,26,2265,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}(), no-evaluators{}()]
   hooked-symbol Lbl'Hash'putc'LParUndsCommUndsRParUnds'K-IO'Unds'K'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortK{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), impure{}(), hook{}("IO.putc"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2447,16,2447,93)"), left{}(), format{}("%c#putc%r %c(%r %1 %c,%r %2 %c)%r"), function{}()]
   hooked-symbol Lbl'Hash'read'LParUndsCommUndsRParUnds'K-IO'Unds'IOString'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortIOString{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), impure{}(), hook{}("IO.read"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2438,23,2438,99)"), left{}(), format{}("%c#read%r %c(%r %1 %c,%r %2 %c)%r"), function{}()]
   hooked-symbol Lbl'Hash'remove'LParUndsRParUnds'K-IO'Unds'K'Unds'String{}(SortString{}) : SortK{} [functional{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}(), priorities{}(), right{}(), terminals{}("1101"), impure{}(), klabel{}("#remove"), hook{}("IO.remove"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2541,16,2541,80)"), left{}(), format{}("%c#remove%r %c(%r %1 %c)%r"), function{}()]
diff --git a/test/regression-c/test-smoke-definition.kore b/test/regression-c/test-smoke-definition.kore
index eb2381f50a..a6181f96a4 100644
--- a/test/regression-c/test-smoke-definition.kore
+++ b/test/regression-c/test-smoke-definition.kore
@@ -1028,7 +1028,7 @@ module C
   symbol Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(SortInt{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#ostream"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2487,21,2487,34)"), left{}(), format{}("%c#ostream%r %c(%r %1 %c)%r"), injective{}()]
   symbol Lbl'Hash'parseInput'LParUndsCommUndsRParUnds'K-IO'Unds'Stream'Unds'String'Unds'String{}(SortString{}, SortString{}) : SortStream{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("110101"), klabel{}("#parseInput"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2486,21,2486,48)"), left{}(), format{}("%c#parseInput%r %c(%r %1 %c,%r %2 %c)%r"), injective{}()]
   hooked-symbol Lbl'Hash'parseKAST'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKAST"), hook{}("KREFLECTION.parseKAST"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2173,26,2173,84)"), left{}(), format{}("%c#parseKAST%r %c(%r %1 %c)%r"), function{}()]
-  hooked-symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), hook{}("KREFLECTION.parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2171,26,2171,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}()]
+  symbol Lbl'Hash'parseKORE'LParUndsRParUnds'K-REFLECTION'Unds'Sort'Unds'String{SortSort}(SortString{}) : SortSort [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), priorities{}(), right{}(), terminals{}("1101"), klabel{}("#parseKORE"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2171,26,2171,84)"), left{}(), format{}("%c#parseKORE%r %c(%r %1 %c)%r"), function{}(), no-evaluators{}()]
   symbol Lbl'Hash'performDeferredChecks'LParRParUnds'C-CHECKER-SYNTAX'Unds'KItem{}() : SortKItem{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/c-semantics/semantics/checker/checker.k)"), priorities{}(), right{}(), terminals{}("111"), klabel{}("#performDeferredChecks"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(18,20,18,44)"), left{}(), format{}("%c#performDeferredChecks%r %c(%r %c)%r"), injective{}()]
   symbol Lbl'Hash'pointerAdditionCheck'LParUndsCommUndsCommUndsRParUnds'C-ADDITIVE-EXP'Unds'KItem'Unds'ObjectId'Unds'Int'Unds'Type{}(SortObjectId{}, SortInt{}, SortType{}) : SortKItem{} [functional{}(), constructor{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/c-semantics/semantics/language/exp/additive.k)"), priorities{}(), right{}(), terminals{}("11010101"), klabel{}("#pointerAdditionCheck"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(39,20,39,62)"), left{}(), format{}("%c#pointerAdditionCheck%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r"), injective{}()]
   symbol Lbl'Hash'promote'LParUndsCommUndsCommUndsRParUnds'C-CONVERSIONS'Unds'Exp'Unds'Exp'Unds'Type'Unds'MaybeInt{}(SortExp{}, SortType{}, SortMaybeInt{}, SortGeneratedTopCell{}) : SortExp{} [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/c-semantics/semantics/language/concepts/conversions.k)"), priorities{}(), right{}(), terminals{}("110101010"), klabel{}("#promote"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(98,18,98,58)"), left{}(), format{}("%c#promote%r %c(%r %1 %c,%r %2 %c,%r %3 %c)%r %4"), function{}()]