diff --git a/kore/src/Kore/Attribute/Overload.hs b/kore/src/Kore/Attribute/Overload.hs
index 427fcd9fbf..e57ade67a7 100644
--- a/kore/src/Kore/Attribute/Overload.hs
+++ b/kore/src/Kore/Attribute/Overload.hs
@@ -36,7 +36,7 @@ instance Default (Overload symbol) where
 
 -- | Kore identifier representing the @overload@ attribute symbol.
 overloadId :: Id
-overloadId = "overload"
+overloadId = "symbol-overload"
 
 -- | Kore symbol representing the @overload@ attribute.
 overloadSymbol :: SymbolOrAlias
diff --git a/kore/test/Test/Kore/Attribute/Overload.hs b/kore/test/Test/Kore/Attribute/Overload.hs
index de31f80b76..5a8f8a44ac 100644
--- a/kore/test/Test/Kore/Attribute/Overload.hs
+++ b/kore/test/Test/Kore/Attribute/Overload.hs
@@ -80,7 +80,7 @@ subSymbolOrAlias = toSymbolOrAlias subSymbol
 
 test_Overload :: TestTree
 test_Overload =
-    testCase "[overload{}(super{}(), sub{}())] :: Overload" $
+    testCase "[symbol-overload{}(super{}(), sub{}())] :: Overload" $
         expectSuccess expected $
             parseOverload attributes
   where
@@ -95,20 +95,20 @@ attributes = Attributes [attribute]
 
 test_Attributes :: TestTree
 test_Attributes =
-    testCase "[overload{}(super{}(), sub{}())] :: Attributes" $
+    testCase "[symbol-overload{}(super{}(), sub{}())] :: Attributes" $
         expectSuccess attributes $
             parseAttributes attributes
 
 test_duplicate :: TestTree
 test_duplicate =
-    testCase "[overload{}(_, _), overload{}(_, _)]" $
+    testCase "[symbol-overload{}(_, _), symbol-overload{}(_, _)]" $
         expectFailure $
             parseOverload $
                 Attributes [attribute, attribute]
 
 test_arguments :: TestTree
 test_arguments =
-    testCase "[overload{}(\"illegal\")]" $
+    testCase "[symbol-overload{}(\"illegal\")]" $
         expectFailure $
             parseOverload $
                 Attributes [illegalAttribute]
@@ -118,7 +118,7 @@ test_arguments =
 
 test_parameters :: TestTree
 test_parameters =
-    testCase "[overload{illegal}()]" $
+    testCase "[symbol-overload{illegal}()]" $
         expectFailure $
             parseOverload $
                 Attributes [illegalAttribute]
diff --git a/test/issue-3508/definition.kore b/test/issue-3508/definition.kore
index a771572b76..79eaef7bd6 100644
--- a/test/issue-3508/definition.kore
+++ b/test/issue-3508/definition.kore
@@ -3762,13 +3762,13 @@ module IMP
   axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortTCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortGeneratedCounterCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortTCellOpt{}, X1:SortGeneratedCounterCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk
   axiom{} \or{SortIOError{}} (Lbl'Hash'E2BIG{}(), \or{SortIOError{}} (Lbl'Hash'EACCES{}(), \or{SortIOError{}} (Lbl'Hash'EADDRINUSE{}(), \or{SortIOError{}} (Lbl'Hash'EADDRNOTAVAIL{}(), \or{SortIOError{}} (Lbl'Hash'EAFNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EAGAIN{}(), \or{SortIOError{}} (Lbl'Hash'EALREADY{}(), \or{SortIOError{}} (Lbl'Hash'EBADF{}(), \or{SortIOError{}} (Lbl'Hash'EBUSY{}(), \or{SortIOError{}} (Lbl'Hash'ECHILD{}(), \or{SortIOError{}} (Lbl'Hash'ECONNABORTED{}(), \or{SortIOError{}} (Lbl'Hash'ECONNREFUSED{}(), \or{SortIOError{}} (Lbl'Hash'ECONNRESET{}(), \or{SortIOError{}} (Lbl'Hash'EDEADLK{}(), \or{SortIOError{}} (Lbl'Hash'EDESTADDRREQ{}(), \or{SortIOError{}} (Lbl'Hash'EDOM{}(), \or{SortIOError{}} (Lbl'Hash'EEXIST{}(), \or{SortIOError{}} (Lbl'Hash'EFAULT{}(), \or{SortIOError{}} (Lbl'Hash'EFBIG{}(), \or{SortIOError{}} (Lbl'Hash'EHOSTDOWN{}(), \or{SortIOError{}} (Lbl'Hash'EHOSTUNREACH{}(), \or{SortIOError{}} (Lbl'Hash'EINPROGRESS{}(), \or{SortIOError{}} (Lbl'Hash'EINTR{}(), \or{SortIOError{}} (Lbl'Hash'EINVAL{}(), \or{SortIOError{}} (Lbl'Hash'EIO{}(), \or{SortIOError{}} (Lbl'Hash'EISCONN{}(), \or{SortIOError{}} (Lbl'Hash'EISDIR{}(), \or{SortIOError{}} (Lbl'Hash'ELOOP{}(), \or{SortIOError{}} (Lbl'Hash'EMFILE{}(), \or{SortIOError{}} (Lbl'Hash'EMLINK{}(), \or{SortIOError{}} (Lbl'Hash'EMSGSIZE{}(), \or{SortIOError{}} (Lbl'Hash'ENAMETOOLONG{}(), \or{SortIOError{}} (Lbl'Hash'ENETDOWN{}(), \or{SortIOError{}} (Lbl'Hash'ENETRESET{}(), \or{SortIOError{}} (Lbl'Hash'ENETUNREACH{}(), \or{SortIOError{}} (Lbl'Hash'ENFILE{}(), \or{SortIOError{}} (Lbl'Hash'ENOBUFS{}(), \or{SortIOError{}} (Lbl'Hash'ENODEV{}(), \or{SortIOError{}} (Lbl'Hash'ENOENT{}(), \or{SortIOError{}} (Lbl'Hash'ENOEXEC{}(), \or{SortIOError{}} (Lbl'Hash'ENOLCK{}(), \or{SortIOError{}} (Lbl'Hash'ENOMEM{}(), \or{SortIOError{}} (Lbl'Hash'ENOPROTOOPT{}(), \or{SortIOError{}} (Lbl'Hash'ENOSPC{}(), \or{SortIOError{}} (Lbl'Hash'ENOSYS{}(), \or{SortIOError{}} (Lbl'Hash'ENOTCONN{}(), \or{SortIOError{}} (Lbl'Hash'ENOTDIR{}(), \or{SortIOError{}} (Lbl'Hash'ENOTEMPTY{}(), \or{SortIOError{}} (Lbl'Hash'ENOTSOCK{}(), \or{SortIOError{}} (Lbl'Hash'ENOTTY{}(), \or{SortIOError{}} (Lbl'Hash'ENXIO{}(), \or{SortIOError{}} (Lbl'Hash'EOF{}(), \or{SortIOError{}} (Lbl'Hash'EOPNOTSUPP{}(), \or{SortIOError{}} (Lbl'Hash'EOVERFLOW{}(), \or{SortIOError{}} (Lbl'Hash'EPERM{}(), \or{SortIOError{}} (Lbl'Hash'EPFNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EPIPE{}(), \or{SortIOError{}} (Lbl'Hash'EPROTONOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'EPROTOTYPE{}(), \or{SortIOError{}} (Lbl'Hash'ERANGE{}(), \or{SortIOError{}} (Lbl'Hash'EROFS{}(), \or{SortIOError{}} (Lbl'Hash'ESHUTDOWN{}(), \or{SortIOError{}} (Lbl'Hash'ESOCKTNOSUPPORT{}(), \or{SortIOError{}} (Lbl'Hash'ESPIPE{}(), \or{SortIOError{}} (Lbl'Hash'ESRCH{}(), \or{SortIOError{}} (Lbl'Hash'ETIMEDOUT{}(), \or{SortIOError{}} (Lbl'Hash'ETOOMANYREFS{}(), \or{SortIOError{}} (Lbl'Hash'EWOULDBLOCK{}(), \or{SortIOError{}} (Lbl'Hash'EXDEV{}(), \or{SortIOError{}} (\exists{SortIOError{}} (X0:SortString{}, Lbl'Hash'noParse{}(X0:SortString{})), \or{SortIOError{}} (\exists{SortIOError{}} (X0:SortInt{}, Lbl'Hash'unknownIOError{}(X0:SortInt{})), \bottom{SortIOError{}}()))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) [constructor{}()] // no junk
   axiom{} \or{SortAExp{}} (\exists{SortAExp{}} (X0:SortId{}, Lbl'PlusPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'Id{}(X0:SortId{})), \or{SortAExp{}} (\exists{SortAExp{}} (X0:SortInt{}, Lbl-'UndsUnds'IMP-SYNTAX'Unds'AExp'Unds'Int{}(X0:SortInt{})), \or{SortAExp{}} (\exists{SortAExp{}} (X0:SortAExp{}, \exists{SortAExp{}} (X1:SortAExp{}, Lbl'UndsPlusUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(X0:SortAExp{}, X1:SortAExp{}))), \or{SortAExp{}} (\exists{SortAExp{}} (X0:SortAExp{}, \exists{SortAExp{}} (X1:SortAExp{}, Lbl'UndsSlshUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'AExp'Unds'AExp{}(X0:SortAExp{}, X1:SortAExp{}))), \or{SortAExp{}} (\exists{SortAExp{}} (X0:SortId{}, \exists{SortAExp{}} (X1:SortAExp{}, Lbl'UndsEqlsUndsUnds'IMP-SYNTAX'Unds'AExp'Unds'Id'Unds'AExp{}(X0:SortId{}, X1:SortAExp{}))), \or{SortAExp{}} (Lblread'LParRParUnds'IMP-SYNTAX'Unds'AExp{}(), \or{SortAExp{}} (\exists{SortAExp{}} (X0:SortBlock{}, Lblspawn'UndsUnds'IMP-SYNTAX'Unds'AExp'Unds'Block{}(X0:SortBlock{})), \or{SortAExp{}} (\exists{SortAExp{}} (Val:SortString{}, inj{SortString{}, SortAExp{}} (Val:SortString{})), \or{SortAExp{}} (\exists{SortAExp{}} (Val:SortPrintable{}, inj{SortPrintable{}, SortAExp{}} (Val:SortPrintable{})), \or{SortAExp{}} (\exists{SortAExp{}} (Val:SortId{}, inj{SortId{}, SortAExp{}} (Val:SortId{})), \or{SortAExp{}} (\exists{SortAExp{}} (Val:SortInt{}, inj{SortInt{}, SortAExp{}} (Val:SortInt{})), \bottom{SortAExp{}}()))))))))))) [constructor{}()] // no junk
-  axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortIds{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())] // overloaded production
-  axiom{R} \equals{SortAExps{}, R} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(inj{SortId{}, SortAExp{}} (K0:SortId{}),inj{SortIds{}, SortAExps{}} (K1:SortIds{})), inj{SortIds{}, SortAExps{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}(K0:SortId{},K1:SortIds{}))) [overload{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}())] // overloaded production
-  axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortPrintables{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}())] // overloaded production
-  axiom{R} \equals{SortIds{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}(), inj{SortBottoms{}, SortIds{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())] // overloaded production
-  axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortBottoms{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())] // overloaded production
-  axiom{R} \equals{SortPrintables{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}(), inj{SortBottoms{}, SortPrintables{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())] // overloaded production
-  axiom{R} \equals{SortAExps{}, R} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(inj{SortPrintable{}, SortAExp{}} (K0:SortPrintable{}),inj{SortPrintables{}, SortAExps{}} (K1:SortPrintables{})), inj{SortPrintables{}, SortAExps{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables{}(K0:SortPrintable{},K1:SortPrintables{}))) [overload{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables{}())] // overloaded production
+  axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortIds{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}())] // overloaded production
+  axiom{R} \equals{SortAExps{}, R} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(inj{SortId{}, SortAExp{}} (K0:SortId{}),inj{SortIds{}, SortAExps{}} (K1:SortIds{})), inj{SortIds{}, SortAExps{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}(K0:SortId{},K1:SortIds{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids{}())] // overloaded production
+  axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortPrintables{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}())] // overloaded production
+  axiom{R} \equals{SortIds{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}(), inj{SortBottoms{}, SortIds{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Ids'Unds'Id'Unds'Ids'QuotRBraUnds'Ids{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())] // overloaded production
+  axiom{R} \equals{SortAExps{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), inj{SortBottoms{}, SortAExps{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps'QuotRBraUnds'AExps{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())] // overloaded production
+  axiom{R} \equals{SortPrintables{}, R} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}(), inj{SortBottoms{}, SortPrintables{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables'QuotRBraUnds'Printables{}(), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'Unds'Bottoms'Unds'Bottom'Unds'Bottoms'QuotRBraUnds'Bottoms{}())] // overloaded production
+  axiom{R} \equals{SortAExps{}, R} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(inj{SortPrintable{}, SortAExp{}} (K0:SortPrintable{}),inj{SortPrintables{}, SortAExps{}} (K1:SortPrintables{})), inj{SortPrintables{}, SortAExps{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables{}(K0:SortPrintable{},K1:SortPrintables{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'AExps'Unds'AExp'Unds'AExps{}(), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'Printables'Unds'Printable'Unds'Printables{}())] // overloaded production
 
 // rules
 // rule `#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort`{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(2b32069ac3f589174502fa507ebc88fab7c902854c0a9baa8ab09beb551232e2), org.kframework.attributes.Location(Location(2222,8,2222,59)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework-5.0.0/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
diff --git a/test/regression-c/test-smoke-definition.kore b/test/regression-c/test-smoke-definition.kore
index a6181f96a4..5c22608e7c 100644
--- a/test/regression-c/test-smoke-definition.kore
+++ b/test/regression-c/test-smoke-definition.kore
@@ -164627,14 +164627,14 @@ module C
   axiom{} \or{SortBstackCellOpt{}} (LblnoBstackCell{}(), \or{SortBstackCellOpt{}} (\exists{SortBstackCellOpt{}} (Val:SortBstackCell{}, inj{SortBstackCell{}, SortBstackCellOpt{}} (Val:SortBstackCell{})), \bottom{SortBstackCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \or{SortFstackCellOpt{}} (LblnoFstackCell{}(), \or{SortFstackCellOpt{}} (\exists{SortFstackCellOpt{}} (Val:SortFstackCell{}, inj{SortFstackCell{}, SortFstackCellOpt{}} (Val:SortFstackCell{})), \bottom{SortFstackCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \or{SortStorageId{}} (Lblallocated'LParRParUnds'C-STORAGE-DURATION-SYNTAX'Unds'StorageId{}(), \or{SortStorageId{}} (\exists{SortStorageId{}} (X0:SortInt{}, Lblauto'LParUndsRParUnds'C-STORAGE-DURATION-SYNTAX'Unds'StorageId'Unds'Int{}(X0:SortInt{})), \or{SortStorageId{}} (Lblstatic'LParRParUnds'C-STORAGE-DURATION-SYNTAX'Unds'StorageId{}(), \or{SortStorageId{}} (\exists{SortStorageId{}} (X0:SortInt{}, Lblthread'LParUndsRParUnds'C-STORAGE-DURATION-SYNTAX'Unds'StorageId'Unds'Int{}(X0:SortInt{})), \bottom{SortStorageId{}}())))) [constructor{}()] // no junk
-  axiom{R} \equals{SortVals{}, R} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}(inj{SortRVals{}, SortVals{}} (K0:SortRVals{}),inj{SortRVal{}, SortVal{}} (K1:SortRVal{})), inj{SortRVals{}, SortVals{}} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}(K0:SortRVals{},K1:SortRVal{}))) [overload{}(Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}(), Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}())] // overloaded production
-  axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(inj{SortRVals{}, SortExps{}} (K0:SortRVals{}),inj{SortRVal{}, SortExp{}} (K1:SortRVal{})), inj{SortRVals{}, SortExps{}} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}(K0:SortRVals{},K1:SortRVal{}))) [overload{}(Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(), Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}())] // overloaded production
-  axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(inj{SortVals{}, SortExps{}} (K0:SortVals{}),inj{SortVal{}, SortExp{}} (K1:SortVal{})), inj{SortVals{}, SortExps{}} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}(K0:SortVals{},K1:SortVal{}))) [overload{}(Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(), Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}())] // overloaded production
-  axiom{R} \equals{SortDirectDeclarator{}, R} (Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'DirectDeclarator'Unds'Declarator{}(inj{SortFunctionDeclarator{}, SortDeclarator{}} (K0:SortFunctionDeclarator{})), inj{SortFunctionDirectDeclarator{}, SortDirectDeclarator{}} (Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'FunctionDirectDeclarator'Unds'FunctionDeclarator{}(K0:SortFunctionDeclarator{}))) [overload{}(Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'DirectDeclarator'Unds'Declarator{}(), Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'FunctionDirectDeclarator'Unds'FunctionDeclarator{}())] // overloaded production
-  axiom{R} \equals{SortExps{}, R} (Lblarg{}(inj{SortVal{}, SortExp{}} (K0:SortVal{})), inj{SortVals{}, SortExps{}} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}(K0:SortVal{}))) [overload{}(Lblarg{}(), Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}())] // overloaded production
-  axiom{R} \equals{SortValue{}, R} (Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'Value'Unds'Value'Unds'String'Unds'KItem{}(inj{SortObjectId{}, SortValue{}} (K0:SortObjectId{}),K1:SortString{},K2:SortKItem{},K3:SortGeneratedTopCell{}), inj{SortObjectId{}, SortValue{}} (Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'ObjectId'Unds'ObjectId'Unds'String'Unds'KItem{}(K0:SortObjectId{},K1:SortString{},K2:SortKItem{},K3:SortGeneratedTopCell{}))) [overload{}(Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'Value'Unds'Value'Unds'String'Unds'KItem{}(), Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'ObjectId'Unds'ObjectId'Unds'String'Unds'KItem{}())] // overloaded production
-  axiom{R} \equals{SortVals{}, R} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}(inj{SortRVal{}, SortVal{}} (K0:SortRVal{})), inj{SortRVals{}, SortVals{}} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}(K0:SortRVal{}))) [overload{}(Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}(), Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}())] // overloaded production
-  axiom{R} \equals{SortExps{}, R} (Lblarg{}(inj{SortRVal{}, SortExp{}} (K0:SortRVal{})), inj{SortRVals{}, SortExps{}} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}(K0:SortRVal{}))) [overload{}(Lblarg{}(), Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}())] // overloaded production
+  axiom{R} \equals{SortVals{}, R} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}(inj{SortRVals{}, SortVals{}} (K0:SortRVals{}),inj{SortRVal{}, SortVal{}} (K1:SortRVal{})), inj{SortRVals{}, SortVals{}} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}(K0:SortRVals{},K1:SortRVal{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}(), Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}())] // overloaded production
+  axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(inj{SortRVals{}, SortExps{}} (K0:SortRVals{}),inj{SortRVal{}, SortExp{}} (K1:SortRVal{})), inj{SortRVals{}, SortExps{}} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}(K0:SortRVals{},K1:SortRVal{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(), Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVals'Unds'RVal{}())] // overloaded production
+  axiom{R} \equals{SortExps{}, R} (Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(inj{SortVals{}, SortExps{}} (K0:SortVals{}),inj{SortVal{}, SortExp{}} (K1:SortVal{})), inj{SortVals{}, SortExps{}} (Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}(K0:SortVals{},K1:SortVal{}))) [symbol-overload{}(Lbl'UndsCommUndsUnds'C-EXPRESSIONS-SYNTAX'Unds'Exps'Unds'Exps'Unds'Exp{}(), Lbl'UndsCommUndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Vals'Unds'Val{}())] // overloaded production
+  axiom{R} \equals{SortDirectDeclarator{}, R} (Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'DirectDeclarator'Unds'Declarator{}(inj{SortFunctionDeclarator{}, SortDeclarator{}} (K0:SortFunctionDeclarator{})), inj{SortFunctionDirectDeclarator{}, SortDirectDeclarator{}} (Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'FunctionDirectDeclarator'Unds'FunctionDeclarator{}(K0:SortFunctionDeclarator{}))) [symbol-overload{}(Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'DirectDeclarator'Unds'Declarator{}(), Lbl'LParUndsRParUnds'C-DECLARATIONS-SYNTAX'Unds'FunctionDirectDeclarator'Unds'FunctionDeclarator{}())] // overloaded production
+  axiom{R} \equals{SortExps{}, R} (Lblarg{}(inj{SortVal{}, SortExp{}} (K0:SortVal{})), inj{SortVals{}, SortExps{}} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}(K0:SortVal{}))) [symbol-overload{}(Lblarg{}(), Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}())] // overloaded production
+  axiom{R} \equals{SortValue{}, R} (Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'Value'Unds'Value'Unds'String'Unds'KItem{}(inj{SortObjectId{}, SortValue{}} (K0:SortObjectId{}),K1:SortString{},K2:SortKItem{},K3:SortGeneratedTopCell{}), inj{SortObjectId{}, SortValue{}} (Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'ObjectId'Unds'ObjectId'Unds'String'Unds'KItem{}(K0:SortObjectId{},K1:SortString{},K2:SortKItem{},K3:SortGeneratedTopCell{}))) [symbol-overload{}(Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'Value'Unds'Value'Unds'String'Unds'KItem{}(), Lblcheck'LParUndsCommUndsCommUndsRParUnds'C-CHECKER-SYNTAX'Unds'ObjectId'Unds'ObjectId'Unds'String'Unds'KItem{}())] // overloaded production
+  axiom{R} \equals{SortVals{}, R} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}(inj{SortRVal{}, SortVal{}} (K0:SortRVal{})), inj{SortRVals{}, SortVals{}} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}(K0:SortRVal{}))) [symbol-overload{}(Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'Vals'Unds'Val{}(), Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}())] // overloaded production
+  axiom{R} \equals{SortExps{}, R} (Lblarg{}(inj{SortRVal{}, SortExp{}} (K0:SortRVal{})), inj{SortRVals{}, SortExps{}} (Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}(K0:SortRVal{}))) [symbol-overload{}(Lblarg{}(), Lbl'UndsUnds'C-REPRESENTATION-SYNTAX'Unds'RVals'Unds'RVal{}())] // overloaded production
 
 // rules
 // rule `<generatedTop>`(`<phase>`(`execute_C-PHASE_Phase`(.KList)) #as _Gen10,`<state>`(`<k>`(`` `simpleAssign(_,_,_)_C-EXPRESSIONS-COMMON_KItem_ObjectId_Value_QualType`(`nativePtr(_)_C-STORAGE-DURATION-SYNTAX_ObjectId_Int`(Addr),V,QT) #as _Gen15``~>_DotVar2),_Gen0,_Gen1,_Gen2,_Gen3,_Gen4,_Gen5),_Gen6,_Gen7,_Gen8) #as #Configuration=>`<generatedTop>`(_Gen10,`<state>`(`<k>`(`check(_,_)_C-CHECKER-SYNTAX_KItem_String_KItem`(#token("\"native_write\"","String"),_Gen15)~>`#nativeWrite(_,_)_FFI_K_Int_Bytes`(Addr,`represent(_,_)_C-REPRESENTATION-SYNTAX_Bytes_Value_Type`(V,`project:qt(_,_)_C-TYPES-SYNTAX_QualType_Set_Type:unqual`(QT),#Configuration))~>_DotVar2),_Gen0,_Gen1,_Gen2,_Gen3,_Gen4,_Gen5),_Gen6,_Gen7,_Gen8) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(882c69c8dbc8e56a5eae2a1651ab36896bd7f28044d7ebba9e95cbd27e774309), org.kframework.attributes.Location(Location(449,8,455,32)), org.kframework.attributes.Source(Source(/home/dwightguth/c-semantics/semantics/language/exp/exp.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
diff --git a/test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore b/test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore
index b344ee82f3..f5c074eefd 100644
--- a/test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore
+++ b/test/regression-evm/test-dsvalue-peek-pass-rough-definition.kore
@@ -13880,8 +13880,8 @@ module VERIFICATION
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`#WordPackAddrUInt48UInt48(_,_,_)_WORD-PACK-COMMON_Int_Int_Int_Int`(ADDR,UINT48_1,UINT48_2))=>#Equals{Bool,#SortParam}(#token("true","Bool"),`_andBool_`(`_andBool_`(`_andBool_`(`_<=Int_`(#token("0","Int"),ADDR),`_<Int_`(ADDR,#token("1461501637330902918203684832716283019655932542976","Int"))),`_andBool_`(`_<=Int_`(#token("0","Int"),UINT48_1),`_<Int_`(UINT48_1,#token("281474976710656","Int")))),`_andBool_`(`_<=Int_`(#token("0","Int"),UINT48_2),`_<Int_`(UINT48_2,#token("281474976710656","Int"))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d18f902b95e68aa34fa454c765bc12e3cf573685fbe0914589ea605c3c17c40c), org.kframework.attributes.Location(Location(79,10,83,9)), org.kframework.attributes.Source(Source(evm-semantics/tests/specs/mcd/word-pack.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore b/test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore
index b344ee82f3..f5c074eefd 100644
--- a/test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore
+++ b/test/regression-evm/test-flipper-addu48u48-fail-rough-definition.kore
@@ -13880,8 +13880,8 @@ module VERIFICATION
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`#WordPackAddrUInt48UInt48(_,_,_)_WORD-PACK-COMMON_Int_Int_Int_Int`(ADDR,UINT48_1,UINT48_2))=>#Equals{Bool,#SortParam}(#token("true","Bool"),`_andBool_`(`_andBool_`(`_andBool_`(`_<=Int_`(#token("0","Int"),ADDR),`_<Int_`(ADDR,#token("1461501637330902918203684832716283019655932542976","Int"))),`_andBool_`(`_<=Int_`(#token("0","Int"),UINT48_1),`_<Int_`(UINT48_1,#token("281474976710656","Int")))),`_andBool_`(`_<=Int_`(#token("0","Int"),UINT48_2),`_<Int_`(UINT48_2,#token("281474976710656","Int"))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d18f902b95e68aa34fa454c765bc12e3cf573685fbe0914589ea605c3c17c40c), org.kframework.attributes.Location(Location(79,10,83,9)), org.kframework.attributes.Source(Source(evm-semantics/tests/specs/mcd/word-pack.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-evm/test-functional-definition.kore b/test/regression-evm/test-functional-definition.kore
index d52c9dfcc1..d57cfcb3e5 100644
--- a/test/regression-evm/test-functional-definition.kore
+++ b/test/regression-evm/test-functional-definition.kore
@@ -13572,8 +13572,8 @@ module FUNCTIONAL-SPEC-SYNTAX
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{Bytes,#SortParam}(`#ecrec(_,_,_,_)_EVM_Bytes_Bytes_Bytes_Bytes_Bytes`(HASH,SIGV,SIGR,SIGS))=>#Top{#SortParam}(.KList) requires `#ecrecEmpty(_,_,_,_)_VERIFICATION-COMMON_Bool_Bytes_Bytes_Bytes_Bytes`(HASH,SIGV,SIGR,SIGS) ensures #token("true","Bool") [UNIQUE_ID(1b9967bfd1f1382881f3f65fd4577d62aacdea3a9abcbe45fd0d85379ca4af40), org.kframework.attributes.Location(Location(23,10,24,50)), org.kframework.attributes.Source(Source(evm-semantics/tests/specs/benchmarks/verification.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-evm/test-lemmas-definition.kore b/test/regression-evm/test-lemmas-definition.kore
index 9f0996f465..4a7991cd09 100644
--- a/test/regression-evm/test-lemmas-definition.kore
+++ b/test/regression-evm/test-lemmas-definition.kore
@@ -13571,8 +13571,8 @@ module VERIFICATION
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{KItem,#SortParam}(`Map:lookup`(@M,@K))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_in_keys(_)_MAP_Bool_KItem_Map`(@K,@M),#token("true","Bool")),#Ceil{Map,#SortParam}(@M)),#Ceil{KItem,#SortParam}(@K)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(64af32ac6f7c97055883b398a4c9381faa0e1941fea1778e6cbb01fde1fc6557), org.kframework.attributes.Location(Location(411,8,411,97)), org.kframework.attributes.Source(Source(evm-semantics/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-evm/test-storagevar03-definition.kore b/test/regression-evm/test-storagevar03-definition.kore
index 38fec338af..be02d7ac6c 100644
--- a/test/regression-evm/test-storagevar03-definition.kore
+++ b/test/regression-evm/test-storagevar03-definition.kore
@@ -13518,8 +13518,8 @@ module VERIFICATION
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{Bytes,#SortParam}(`#ecrec(_,_,_,_)_EVM_Bytes_Bytes_Bytes_Bytes_Bytes`(HASH,SIGV,SIGR,SIGS))=>#Top{#SortParam}(.KList) requires `#ecrecEmpty(_,_,_,_)_VERIFICATION-COMMON_Bool_Bytes_Bytes_Bytes_Bytes`(HASH,SIGV,SIGR,SIGS) ensures #token("true","Bool") [UNIQUE_ID(1b9967bfd1f1382881f3f65fd4577d62aacdea3a9abcbe45fd0d85379ca4af40), org.kframework.attributes.Location(Location(23,10,24,50)), org.kframework.attributes.Source(Source(evm-semantics/tests/specs/benchmarks/verification.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-evm/test-sum-to-n-definition.kore b/test/regression-evm/test-sum-to-n-definition.kore
index 9c21e8dcbf..0cb2a71633 100644
--- a/test/regression-evm/test-sum-to-n-definition.kore
+++ b/test/regression-evm/test-sum-to-n-definition.kore
@@ -8074,8 +8074,8 @@ module VERIFICATION
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{KItem,#SortParam}(`Map:lookup`(@M,@K))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_in_keys(_)_MAP_Bool_KItem_Map`(@K,@M),#token("true","Bool")),#Ceil{Map,#SortParam}(@M)),#Ceil{KItem,#SortParam}(@K)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(64af32ac6f7c97055883b398a4c9381faa0e1941fea1778e6cbb01fde1fc6557), org.kframework.attributes.Location(Location(411,8,411,97)), org.kframework.attributes.Source(Source(evm-semantics/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-evm/test-totalSupply-definition.kore b/test/regression-evm/test-totalSupply-definition.kore
index 59776d6acc..47815ea52b 100644
--- a/test/regression-evm/test-totalSupply-definition.kore
+++ b/test/regression-evm/test-totalSupply-definition.kore
@@ -13516,8 +13516,8 @@ module VERIFICATION
   axiom{} \right-assoc{}(\or{SortMixHashCellOpt{}} (LblnoMixHashCell{}(), \exists{SortMixHashCellOpt{}} (Val:SortMixHashCell{}, inj{SortMixHashCell{}, SortMixHashCellOpt{}} (Val:SortMixHashCell{})), \bottom{SortMixHashCellOpt{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTernStackOp{}} (LblADDMOD'Unds'EVM'Unds'TernStackOp{}(), LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp{}(), LblCODECOPY'Unds'EVM'Unds'TernStackOp{}(), LblCREATE'Unds'EVM'Unds'TernStackOp{}(), LblMULMOD'Unds'EVM'Unds'TernStackOp{}(), LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp{}(), \bottom{SortTernStackOp{}}())) [constructor{}()] // no junk
   axiom{} \right-assoc{}(\or{SortTxType{}} (Lbl'Stop'TxType'Unds'EVM-TYPES'Unds'TxType{}(), LblAccessList'Unds'EVM-TYPES'Unds'TxType{}(), LblDynamicFee'Unds'EVM-TYPES'Unds'TxType{}(), LblLegacy'Unds'EVM-TYPES'Unds'TxType{}(), \bottom{SortTxType{}}())) [constructor{}()] // no junk
-  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(K0:SortSchedule{},inj{SortInt{}, SortGas{}} (K1:SortInt{}),inj{SortInt{}, SortGas{}} (K2:SortInt{}),K3:SortInt{}), inj{SortInt{}, SortGas{}} (LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}(K0:SortSchedule{},K1:SortInt{},K2:SortInt{},K3:SortInt{}))) [symbol-overload{}(LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Schedule'Unds'Gas'Unds'Gas'Unds'Int{}(), LblCgascap'LParUndsCommUndsCommUndsCommUndsRParUnds'GAS-FEES'Unds'Int'Unds'Schedule'Unds'Int'Unds'Int'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortGas{}, R} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(inj{SortInt{}, SortGas{}} (K0:SortInt{})), inj{SortInt{}, SortGas{}} (Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}(K0:SortInt{}))) [symbol-overload{}(Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Gas'Unds'Gas{}(), Lbl'Hash'allBut64th'LParUndsRParUnds'GAS-FEES'Unds'Int'Unds'Int{}())] // overloaded production
 
 // rules
 // rule #Ceil{KItem,#SortParam}(`Map:lookup`(@M,@K))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_in_keys(_)_MAP_Bool_KItem_Map`(@K,@M),#token("true","Bool")),#Ceil{Map,#SortParam}(@M)),#Ceil{KItem,#SortParam}(@K)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(64af32ac6f7c97055883b398a4c9381faa0e1941fea1778e6cbb01fde1fc6557), org.kframework.attributes.Location(Location(411,8,411,97)), org.kframework.attributes.Source(Source(evm-semantics/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-wasm/test-locals-vdefinition.kore b/test/regression-wasm/test-locals-vdefinition.kore
index ee8f288f3b..860f3386a3 100644
--- a/test/regression-wasm/test-locals-vdefinition.kore
+++ b/test/regression-wasm/test-locals-vdefinition.kore
@@ -4538,18 +4538,18 @@ module KWASM-LEMMAS
   axiom{} \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds's{}(), \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds'u{}(), \or{SortCvti64Op{}} (LblaWrap'Unds'i64{}(), \bottom{SortCvti64Op{}}()))) [constructor{}()] // no junk
   axiom{} \or{SortMmaxCell{}} (\exists{SortMmaxCell{}} (X0:SortOptionalInt{}, Lbl'-LT-'mmax'-GT-'{}(X0:SortOptionalInt{})), \bottom{SortMmaxCell{}}()) [constructor{}()] // no junk
   axiom{} \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (X0:SortValType{}, Lbl'LPar'mut'UndsRParUnds'WASM-TEXT-COMMON-SYNTAX'Unds'TextFormatGlobalType'Unds'ValType{}(X0:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortValType{}, inj{SortValType{}, SortTextFormatGlobalType{}} (Val:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortFValType{}, inj{SortFValType{}, SortTextFormatGlobalType{}} (Val:SortFValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortIValType{}, inj{SortIValType{}, SortTextFormatGlobalType{}} (Val:SortIValType{})), \bottom{SortTextFormatGlobalType{}}())))) [constructor{}()] // no junk
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1072,8,1072,102)), org.kframework.attributes.Source(Source(/usr/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-wasm/test-loops-vdefinition.kore b/test/regression-wasm/test-loops-vdefinition.kore
index ee8f288f3b..860f3386a3 100644
--- a/test/regression-wasm/test-loops-vdefinition.kore
+++ b/test/regression-wasm/test-loops-vdefinition.kore
@@ -4538,18 +4538,18 @@ module KWASM-LEMMAS
   axiom{} \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds's{}(), \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds'u{}(), \or{SortCvti64Op{}} (LblaWrap'Unds'i64{}(), \bottom{SortCvti64Op{}}()))) [constructor{}()] // no junk
   axiom{} \or{SortMmaxCell{}} (\exists{SortMmaxCell{}} (X0:SortOptionalInt{}, Lbl'-LT-'mmax'-GT-'{}(X0:SortOptionalInt{})), \bottom{SortMmaxCell{}}()) [constructor{}()] // no junk
   axiom{} \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (X0:SortValType{}, Lbl'LPar'mut'UndsRParUnds'WASM-TEXT-COMMON-SYNTAX'Unds'TextFormatGlobalType'Unds'ValType{}(X0:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortValType{}, inj{SortValType{}, SortTextFormatGlobalType{}} (Val:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortFValType{}, inj{SortFValType{}, SortTextFormatGlobalType{}} (Val:SortFValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortIValType{}, inj{SortIValType{}, SortTextFormatGlobalType{}} (Val:SortIValType{})), \bottom{SortTextFormatGlobalType{}}())))) [constructor{}()] // no junk
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1072,8,1072,102)), org.kframework.attributes.Source(Source(/usr/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-wasm/test-memory-vdefinition.kore b/test/regression-wasm/test-memory-vdefinition.kore
index 2031b01c4a..53948e7426 100644
--- a/test/regression-wasm/test-memory-vdefinition.kore
+++ b/test/regression-wasm/test-memory-vdefinition.kore
@@ -4538,18 +4538,18 @@ module KWASM-LEMMAS
   axiom{} \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds's{}(), \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds'u{}(), \or{SortCvti64Op{}} (LblaWrap'Unds'i64{}(), \bottom{SortCvti64Op{}}()))) [constructor{}()] // no junk
   axiom{} \or{SortMmaxCell{}} (\exists{SortMmaxCell{}} (X0:SortOptionalInt{}, Lbl'-LT-'mmax'-GT-'{}(X0:SortOptionalInt{})), \bottom{SortMmaxCell{}}()) [constructor{}()] // no junk
   axiom{} \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (X0:SortValType{}, Lbl'LPar'mut'UndsRParUnds'WASM-TEXT-COMMON-SYNTAX'Unds'TextFormatGlobalType'Unds'ValType{}(X0:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortValType{}, inj{SortValType{}, SortTextFormatGlobalType{}} (Val:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortFValType{}, inj{SortFValType{}, SortTextFormatGlobalType{}} (Val:SortFValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortIValType{}, inj{SortIValType{}, SortTextFormatGlobalType{}} (Val:SortIValType{})), \bottom{SortTextFormatGlobalType{}}())))) [constructor{}()] // no junk
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1072,8,1072,102)), org.kframework.attributes.Source(Source(/usr/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-wasm/test-simple-arithmetic-vdefinition.kore b/test/regression-wasm/test-simple-arithmetic-vdefinition.kore
index ee8f288f3b..860f3386a3 100644
--- a/test/regression-wasm/test-simple-arithmetic-vdefinition.kore
+++ b/test/regression-wasm/test-simple-arithmetic-vdefinition.kore
@@ -4538,18 +4538,18 @@ module KWASM-LEMMAS
   axiom{} \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds's{}(), \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds'u{}(), \or{SortCvti64Op{}} (LblaWrap'Unds'i64{}(), \bottom{SortCvti64Op{}}()))) [constructor{}()] // no junk
   axiom{} \or{SortMmaxCell{}} (\exists{SortMmaxCell{}} (X0:SortOptionalInt{}, Lbl'-LT-'mmax'-GT-'{}(X0:SortOptionalInt{})), \bottom{SortMmaxCell{}}()) [constructor{}()] // no junk
   axiom{} \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (X0:SortValType{}, Lbl'LPar'mut'UndsRParUnds'WASM-TEXT-COMMON-SYNTAX'Unds'TextFormatGlobalType'Unds'ValType{}(X0:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortValType{}, inj{SortValType{}, SortTextFormatGlobalType{}} (Val:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortFValType{}, inj{SortFValType{}, SortTextFormatGlobalType{}} (Val:SortFValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortIValType{}, inj{SortIValType{}, SortTextFormatGlobalType{}} (Val:SortIValType{})), \bottom{SortTextFormatGlobalType{}}())))) [constructor{}()] // no junk
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1072,8,1072,102)), org.kframework.attributes.Source(Source(/usr/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]
diff --git a/test/regression-wasm/test-wrc20-vdefinition.kore b/test/regression-wasm/test-wrc20-vdefinition.kore
index 16316fbe33..f5e1eb6b09 100644
--- a/test/regression-wasm/test-wrc20-vdefinition.kore
+++ b/test/regression-wasm/test-wrc20-vdefinition.kore
@@ -4556,18 +4556,18 @@ module WRC20-LEMMAS
   axiom{} \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds's{}(), \or{SortCvti64Op{}} (LblaConvert'Unds'i64'Unds'u{}(), \or{SortCvti64Op{}} (LblaWrap'Unds'i64{}(), \bottom{SortCvti64Op{}}()))) [constructor{}()] // no junk
   axiom{} \or{SortMmaxCell{}} (\exists{SortMmaxCell{}} (X0:SortOptionalInt{}, Lbl'-LT-'mmax'-GT-'{}(X0:SortOptionalInt{})), \bottom{SortMmaxCell{}}()) [constructor{}()] // no junk
   axiom{} \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (X0:SortValType{}, Lbl'LPar'mut'UndsRParUnds'WASM-TEXT-COMMON-SYNTAX'Unds'TextFormatGlobalType'Unds'ValType{}(X0:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortValType{}, inj{SortValType{}, SortTextFormatGlobalType{}} (Val:SortValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortFValType{}, inj{SortFValType{}, SortTextFormatGlobalType{}} (Val:SortFValType{})), \or{SortTextFormatGlobalType{}} (\exists{SortTextFormatGlobalType{}} (Val:SortIValType{}, inj{SortIValType{}, SortTextFormatGlobalType{}} (Val:SortIValType{})), \bottom{SortTextFormatGlobalType{}}())))) [constructor{}()] // no junk
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
-  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
-  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
-  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortInstr{}, SortStmt{}} (K0:SortInstr{}),inj{SortInstrs{}, SortStmts{}} (K1:SortInstrs{})), inj{SortInstrs{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(K0:SortInstr{},K1:SortInstrs{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortDefns{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), inj{SortEmptyStmts{}, SortDefns{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns'QuotRBraUnds'Defns{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), inj{SortEmptyStmts{}, SortInstrs{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortEmptyStmts{}, SortStmts{}} (Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuot'listStmt'QuotRBraUnds'EmptyStmts{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortFValType{}, SortValType{}} (K0:SortFValType{}),inj{SortFloat{}, SortNumber{}} (K1:SortFloat{})), inj{SortFVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}(K0:SortFValType{},K1:SortFloat{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'FVal'Unds'FValType'Unds'Float{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), inj{SortInstrs{}, SortStmts{}} (Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())) [symbol-overload{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts'QuotRBraUnds'Stmts{}(), Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs'QuotRBraUnds'Instrs{}())] // overloaded production
+  axiom{R} \equals{SortInstrs{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortEmptyStmt{}, SortInstr{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortInstrs{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortInstrs{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Instrs'Unds'Instr'Unds'Instrs{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortDefns{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(inj{SortEmptyStmt{}, SortDefn{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortDefns{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortDefns{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortEmptyStmt{}, SortStmt{}} (K0:SortEmptyStmt{}),inj{SortEmptyStmts{}, SortStmts{}} (K1:SortEmptyStmts{})), inj{SortEmptyStmts{}, SortStmts{}} (LbllistStmt{}(K0:SortEmptyStmt{},K1:SortEmptyStmts{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), LbllistStmt{}())] // overloaded production
+  axiom{R} \equals{SortVal{}, R} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(inj{SortIValType{}, SortValType{}} (K0:SortIValType{}),inj{SortInt{}, SortNumber{}} (K1:SortInt{})), inj{SortIVal{}, SortVal{}} (Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}(K0:SortIValType{},K1:SortInt{}))) [symbol-overload{}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'ValType'Unds'Number{}(), Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'IVal'Unds'IValType'Unds'Int{}())] // overloaded production
+  axiom{R} \equals{SortStmts{}, R} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(inj{SortDefn{}, SortStmt{}} (K0:SortDefn{}),inj{SortDefns{}, SortStmts{}} (K1:SortDefns{})), inj{SortDefns{}, SortStmts{}} (Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}(K0:SortDefn{},K1:SortDefns{}))) [symbol-overload{}(Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Stmts'Unds'Stmt'Unds'Stmts{}(), Lbl'UndsUndsUnds'WASM-COMMON-SYNTAX'Unds'Defns'Unds'Defn'Unds'Defns{}())] // overloaded production
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1072,8,1072,102)), org.kframework.attributes.Source(Source(/usr/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]