diff --git a/pyk/k-files/regex-terminal.k b/pyk/k-files/regex-terminal.k
new file mode 100644
index 00000000000..faa434101aa
--- /dev/null
+++ b/pyk/k-files/regex-terminal.k
@@ -0,0 +1,11 @@
+module REGEX-TERMINAL-SYNTAX
+    syntax T0 ::= r"b"            [token]
+    syntax T1 ::= r"(?<!a)b"      [token]
+    syntax T2 ::= r"b(?!c)"       [token]
+    syntax T3 ::= r"(?<!a)b(?!c)" [token]
+endmodule
+
+
+module REGEX-TERMINAL
+    imports REGEX-TERMINAL-SYNTAX
+endmodule
diff --git a/pyk/src/pyk/integration_tests/kompiled_test.py b/pyk/src/pyk/integration_tests/kompiled_test.py
index e11a705b493..2b624d94595 100644
--- a/pyk/src/pyk/integration_tests/kompiled_test.py
+++ b/pyk/src/pyk/integration_tests/kompiled_test.py
@@ -1,10 +1,12 @@
+import json
 import shutil
 from abc import ABC
 from pathlib import Path
 from typing import Iterable, Optional
 from unittest import TestCase
 
-from ..ktool import KompileBackend, kompile
+from pyk.kast import KDefinition
+from pyk.ktool import KompileBackend, kompile
 
 
 class KompiledTest(TestCase, ABC):
@@ -13,6 +15,7 @@ class KompiledTest(TestCase, ABC):
     KOMPILE_OUTPUT_DIR: Optional[str] = None
     KOMPILE_INCLUDE_DIRS: Iterable[str] = []
     KOMPILE_EMIT_JSON = False
+    KOMPILE_POST_PROCESS: Optional[str] = None
 
     def setUp(self):
         main_file = Path(self.KOMPILE_MAIN_FILE)
@@ -30,7 +33,13 @@ def setUp(self):
             output_dir=output_dir,
             include_dirs=include_dirs,
             emit_json=self.KOMPILE_EMIT_JSON,
+            post_process=self.KOMPILE_POST_PROCESS,
         )
 
+        if self.KOMPILE_EMIT_JSON:
+            with open(self.kompiled_dir / 'compiled.json', 'r') as f:
+                json_dct = json.load(f)
+                self.definition = KDefinition.from_dict(json_dct['term'])
+
     def tearDown(self):
         shutil.rmtree(self.kompiled_dir)
diff --git a/pyk/src/pyk/integration_tests/test_regex_terminal.py b/pyk/src/pyk/integration_tests/test_regex_terminal.py
new file mode 100644
index 00000000000..aed9a58f9c1
--- /dev/null
+++ b/pyk/src/pyk/integration_tests/test_regex_terminal.py
@@ -0,0 +1,36 @@
+from pyk.kast import KRegexTerminal
+from pyk.ktool import KompileBackend
+
+from .kompiled_test import KompiledTest
+
+
+class RegexTerminalTest(KompiledTest):
+    KOMPILE_MAIN_FILE = 'k-files/regex-terminal.k'
+    KOMPILE_BACKEND = KompileBackend.HASKELL
+    KOMPILE_OUTPUT_DIR = 'definitions/regex-terminal'
+    KOMPILE_EMIT_JSON = True
+    KOMPILE_POST_PROCESS = 'cat'  # This ensures that the compiled JSON is read back by K
+
+    def test(self):
+        # Given
+        expected = [
+            KRegexTerminal('b', '#', '#'),
+            KRegexTerminal('b', 'a', '#'),
+            KRegexTerminal('b', '#', 'c'),
+            KRegexTerminal('b', 'a', 'c'),
+        ]
+
+        module = [module for module in self.definition if module.name == 'REGEX-TERMINAL-SYNTAX'][0]
+        productions = sorted(
+            (
+                prod for prod in module.productions
+                if prod.sort.name in {'T0', 'T1', 'T2', 'T3'}
+                and type(prod.items[0]) is KRegexTerminal  # noqa: W503
+            ),
+            key=lambda prod: prod.sort.name,
+        )
+
+        actual = [prod.items[0] for prod in productions]
+
+        # Then
+        self.assertListEqual(expected, actual)
diff --git a/pyk/src/pyk/kast.py b/pyk/src/pyk/kast.py
index ad0f01533dd..33af0489050 100644
--- a/pyk/src/pyk/kast.py
+++ b/pyk/src/pyk/kast.py
@@ -24,7 +24,7 @@
     overload,
 )
 
-from .utils import FrozenDict, hash_str
+from .utils import FrozenDict, filter_none, hash_str
 
 T = TypeVar('T', bound='KAst')
 W = TypeVar('W', bound='WithKAtt')
@@ -227,23 +227,32 @@ def pretty(self, kprint) -> Iterable[str]:
 
 @final
 @dataclass(frozen=True)
-class KVariable(KInner):
+class KVariable(KInner, WithKAtt):
     name: str
+    att: KAtt
 
-    def __init__(self, name: str):
+    def __init__(self, name: str, att: KAtt = EMPTY_ATT):
         object.__setattr__(self, 'name', name)
+        object.__setattr__(self, 'att', att)
 
     @classmethod
     def from_dict(cls: Type['KVariable'], d: Dict[str, Any]) -> 'KVariable':
         cls._check_node(d)
-        return KVariable(name=d['name'])
+        return KVariable(
+            name=d['name'],
+            att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
+        )
 
     def to_dict(self) -> Dict[str, Any]:
-        return {'node': 'KVariable', 'name': self.name}
+        return {'node': 'KVariable', 'name': self.name, 'att': self.att.to_dict()}
 
-    def let(self, *, name: Optional[str] = None) -> 'KVariable':
+    def let(self, *, name: Optional[str] = None, att: Optional[KAtt] = None) -> 'KVariable':
         name = name if name is not None else self.name
-        return KVariable(name=name)
+        att = att if att is not None else self.att
+        return KVariable(name=name, att=att)
+
+    def let_att(self, att: KAtt) -> 'KVariable':
+        return self.let(att=att)
 
     def map_inner(self: 'KVariable', f: Callable[[KInner], KInner]) -> 'KVariable':
         return self
@@ -491,13 +500,14 @@ def match(self, term: KInner) -> Optional[Subst]:
 
 @final
 @dataclass(frozen=True)
-class KRewrite(KInner):
+class KRewrite(KInner, WithKAtt):
     lhs: KInner
     rhs: KInner
 
-    def __init__(self, lhs: KInner, rhs: KInner):
+    def __init__(self, lhs: KInner, rhs: KInner, att=EMPTY_ATT):
         object.__setattr__(self, 'lhs', lhs)
         object.__setattr__(self, 'rhs', rhs)
+        object.__setattr__(self, 'att', att)
 
     def __iter__(self) -> Iterator[KInner]:
         return iter([self.lhs, self.rhs])
@@ -511,15 +521,34 @@ def __call__(self, term: KInner, *, top=False) -> KInner:
     @classmethod
     def from_dict(cls: Type['KRewrite'], d: Dict[str, Any]) -> 'KRewrite':
         cls._check_node(d)
-        return KRewrite(lhs=KInner.from_dict(d['lhs']), rhs=KInner.from_dict(d['rhs']))
+        return KRewrite(
+            lhs=KInner.from_dict(d['lhs']),
+            rhs=KInner.from_dict(d['rhs']),
+            att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
+        )
 
     def to_dict(self) -> Dict[str, Any]:
-        return {'node': 'KRewrite', 'lhs': self.lhs.to_dict(), 'rhs': self.rhs.to_dict()}
+        return {
+            'node': 'KRewrite',
+            'lhs': self.lhs.to_dict(),
+            'rhs': self.rhs.to_dict(),
+            'att': self.att.to_dict(),
+        }
 
-    def let(self, *, lhs: Optional[KInner] = None, rhs: Optional[KInner] = None) -> 'KRewrite':
+    def let(
+        self,
+        *,
+        lhs: Optional[KInner] = None,
+        rhs: Optional[KInner] = None,
+        att: Optional[KAtt] = None,
+    ) -> 'KRewrite':
         lhs = lhs if lhs is not None else self.lhs
         rhs = rhs if rhs is not None else self.rhs
-        return KRewrite(lhs=lhs, rhs=rhs)
+        att = att if att is not None else self.att
+        return KRewrite(lhs=lhs, rhs=rhs, att=att)
+
+    def let_att(self, att: KAtt) -> 'KRewrite':
+        return self.let(att=att)
 
     def map_inner(self: 'KRewrite', f: Callable[[KInner], KInner]) -> 'KRewrite':
         return self.let(lhs=f(self.lhs), rhs=f(self.rhs))
@@ -728,7 +757,7 @@ class KRegexTerminal(KProductionItem):
     precede_regex: str
     follow_regex: str
 
-    def __init__(self, regex: str, precede_regex: str = '', follow_regex: str = ''):
+    def __init__(self, regex: str, precede_regex: str, follow_regex: str):
         object.__setattr__(self, 'regex', regex)
         object.__setattr__(self, 'precede_regex', precede_regex)
         object.__setattr__(self, 'follow_regex', follow_regex)
@@ -738,14 +767,13 @@ def from_dict(cls: Type['KRegexTerminal'], d: Dict[str, Any]) -> 'KRegexTerminal
         cls._check_node(d)
         return KRegexTerminal(
             regex=d['regex'],
-            precede_regex=d.get('precede_regex', ''),
-            follow_regex=d.get('follow_regex', ''),
+            precede_regex=d['precedeRegex'],
+            follow_regex=d['followRegex'],
         )
 
     def to_dict(self) -> Dict[str, Any]:
-        return {'node': 'KRegexTerminal', 'regex': self.regex, 'precedeRegex': self.precede_regex or None, 'follow_regex': self.follow_regex or None}
+        return {'node': 'KRegexTerminal', 'regex': self.regex, 'precedeRegex': self.precede_regex, 'followRegex': self.follow_regex}
 
-    # TODO consider nullable fields and make sure their value can be erased
     def let(self, *, regex: Optional[str] = None, precede_regex: Optional[str] = None, follow_regex: Optional[str] = None) -> 'KRegexTerminal':
         regex = regex if regex is not None else self.regex
         precede_regex = precede_regex if precede_regex is not None else self.precede_regex
@@ -777,19 +805,31 @@ def let(self, *, sort: Optional[KSort] = None) -> 'KNonTerminal':
 @final
 @dataclass(frozen=True)
 class KProduction(KSentence):
+    # TODO Order in Java implementation: klabel, params, sort, items, att
     sort: KSort
     items: Tuple[KProductionItem, ...]
+    params: Tuple[KSort, ...]
     klabel: Optional[KLabel]
     att: KAtt
 
-    def __init__(self, sort: Union[str, KSort], items: Iterable[KProductionItem] = (), klabel: Optional[Union[str, KLabel]] = None, att=EMPTY_ATT):
+    def __init__(
+        self,
+        sort: Union[str, KSort],
+        items: Iterable[KProductionItem] = (),
+        params: Iterable[Union[str, KSort]] = (),
+        klabel: Optional[Union[str, KLabel]] = None,
+        att=EMPTY_ATT,
+    ):
         if type(sort) is str:
             sort = KSort(sort)
         if type(klabel) is str:
             klabel = KLabel(klabel)
 
+        params = tuple(KSort(param) if type(param) is str else param for param in params)
+
         object.__setattr__(self, 'sort', sort)
         object.__setattr__(self, 'items', tuple(items))
+        object.__setattr__(self, 'params', params)
         object.__setattr__(self, 'klabel', klabel)
         object.__setattr__(self, 'att', att)
 
@@ -803,32 +843,36 @@ def from_dict(cls: Type['KProduction'], d: Dict[str, Any]) -> 'KProduction':
         return KProduction(
             sort=KSort.from_dict(d['sort']),
             items=(KProductionItem.from_dict(item) for item in d['productionItems']),
+            params=(KSort.from_dict(param) for param in d['params']),
             klabel=KLabel.from_dict(d['klabel']) if d.get('klabel') else None,
             att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
         )
 
     def to_dict(self) -> Dict[str, Any]:
-        return {
+        return filter_none({
             'node': 'KProduction',
             'sort': self.sort.to_dict(),
             'productionItems': [item.to_dict() for item in self.items],
+            'params': [param.to_dict() for param in self.params],
             'klabel': self.klabel.to_dict() if self.klabel else None,
             'att': self.att.to_dict(),
-        }
+        })
 
     def let(
         self,
         *,
         sort: Optional[Union[str, KSort]] = None,
         items: Optional[Iterable[KProductionItem]] = None,
+        params: Optional[Iterable[Union[str, KSort]]] = None,
         klabel: Optional[Union[str, KLabel]] = None,
         att: Optional[KAtt] = None,
     ) -> 'KProduction':
         sort = sort if sort is not None else self.sort
         items = items if items is not None else self.items
+        params = params if params is not None else self.params
         klabel = klabel if klabel is not None else self.klabel  # TODO figure out a way to set klabel to None
         att = att if att is not None else self.att
-        return KProduction(sort=sort, items=items, klabel=klabel, att=att)
+        return KProduction(sort=sort, items=items, params=params, klabel=klabel, att=att)
 
     def let_att(self, att: KAtt) -> 'KProduction':
         return self.let(att=att)
@@ -838,24 +882,43 @@ def let_att(self, att: KAtt) -> 'KProduction':
 @dataclass(frozen=True)
 class KSyntaxSort(KSentence):
     sort: KSort
+    params: Tuple[KSort, ...]
     att: KAtt
 
-    def __init__(self, sort: KSort, att=EMPTY_ATT):
+    def __init__(self, sort: KSort, params: Iterable[Union[str, KSort]] = (), att=EMPTY_ATT):
+        params = tuple(KSort(param) if type(param) is str else param for param in params)
         object.__setattr__(self, 'sort', sort)
+        object.__setattr__(self, 'params', params)
         object.__setattr__(self, 'att', att)
 
     @classmethod
     def from_dict(cls: Type['KSyntaxSort'], d: Dict[str, Any]) -> 'KSyntaxSort':
         cls._check_node(d)
-        return KSyntaxSort(sort=KSort.from_dict(d['sort']), att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT)
+        return KSyntaxSort(
+            sort=KSort.from_dict(d['sort']),
+            params=(KSort.from_dict(param) for param in d['params']),
+            att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
+        )
 
     def to_dict(self) -> Dict[str, Any]:
-        return {'node': 'KSyntaxSort', 'sort': self.sort.to_dict(), 'att': self.att.to_dict()}
+        return {
+            'node': 'KSyntaxSort',
+            'sort': self.sort.to_dict(),
+            'params': [param.to_dict() for param in self.params],
+            'att': self.att.to_dict(),
+        }
 
-    def let(self, *, sort: Optional[KSort] = None, att: Optional[KAtt] = None) -> 'KSyntaxSort':
+    def let(
+        self,
+        *,
+        sort: Optional[KSort] = None,
+        params: Optional[Iterable[Union[str, KSort]]] = None,
+        att: Optional[KAtt] = None,
+    ) -> 'KSyntaxSort':
         sort = sort or self.sort
+        params = params if params is not None else self.params
         att = att if att is not None else self.att
-        return KSyntaxSort(sort=sort, att=att)
+        return KSyntaxSort(sort=sort, params=params, att=att)
 
     def let_att(self, att: KAtt) -> 'KSyntaxSort':
         return self.let(att=att)
@@ -1278,6 +1341,7 @@ def from_dict(cls: Type['KFlatModule'], d: Dict[str, Any]) -> 'KFlatModule':
     def to_dict(self) -> Dict[str, Any]:
         return {
             'node': 'KFlatModule',
+            'name': self.name,
             'localSentences': [sentence.to_dict() for sentence in self.sentences],
             'imports': [imp.to_dict() for imp in self.imports],
             'att': self.att.to_dict(),
diff --git a/pyk/src/pyk/ktool/kompile.py b/pyk/src/pyk/ktool/kompile.py
index d9f30f5646f..38c8fb4a0ff 100644
--- a/pyk/src/pyk/ktool/kompile.py
+++ b/pyk/src/pyk/ktool/kompile.py
@@ -1,4 +1,5 @@
 import logging
+import shlex
 from enum import Enum
 from pathlib import Path
 from subprocess import CalledProcessError, CompletedProcess
@@ -27,6 +28,7 @@ def kompile(
     md_selector: Optional[str] = None,
     hook_namespaces: Iterable[str] = (),
     emit_json=False,
+    post_process: Optional[str] = None,
     concrete_rules: Iterable[str] = (),
     additional_args: Iterable[str] = (),
 ) -> Path:
@@ -44,6 +46,7 @@ def kompile(
         md_selector=md_selector,
         hook_namespaces=hook_namespaces,
         emit_json=emit_json,
+        post_process=post_process,
         concrete_rules=concrete_rules,
         additional_args=additional_args
     )
@@ -67,7 +70,8 @@ def _build_arg_list(
     include_dirs: Iterable[Path],
     md_selector: Optional[str],
     hook_namespaces: Iterable[str],
-    emit_json,
+    emit_json: bool,
+    post_process: Optional[str],
     concrete_rules: Iterable[str],
     additional_args: Iterable[str]
 ) -> List[str]:
@@ -97,6 +101,9 @@ def _build_arg_list(
     if emit_json:
         args.append('--emit-json')
 
+    if post_process:
+        args.extend(['--post-process', shlex.quote(post_process)])
+
     if concrete_rules:
         args.extend(['--concrete-rules', ','.join(concrete_rules)])
 
diff --git a/pyk/src/pyk/tests/test_kastManip.py b/pyk/src/pyk/tests/test_kastManip.py
index 28cc64aa2cb..677ccf121cb 100644
--- a/pyk/src/pyk/tests/test_kastManip.py
+++ b/pyk/src/pyk/tests/test_kastManip.py
@@ -107,9 +107,9 @@ def test_ml_pred_to_bool(self):
             (False, KApply(KLabel('#Not', [Sorts.GENERATED_TOP_CELL]), [mlTop()]), KApply('notBool_', [TRUE])),
             (True, KApply(KLabel('#Equals'), [f(a), f(x)]), KApply('_==K_', [f(a), f(x)])),
             (False, KApply(KLabel('#And', [Sorts.GENERATED_TOP_CELL]), [mlEqualsTrue(TRUE), mlEqualsTrue(TRUE)]), KApply('_andBool_', [TRUE, TRUE])),
-            (True, KApply(KLabel('#Ceil', [KSort('Set'), Sorts.GENERATED_TOP_CELL]), [KApply(KLabel('_Set_', [KVariable('_'), KVariable('_')]))]), KVariable('Ceil_d06736ac')),
-            (True, KApply(KLabel('#Not', [Sorts.GENERATED_TOP_CELL]), [KApply(KLabel('#Ceil', [KSort('Set'), Sorts.GENERATED_TOP_CELL]), [KApply(KLabel('_Set_', [KVariable('_'), KVariable('_')]))])]), KApply('notBool_', [KVariable('Ceil_d06736ac')])),
-            (True, KApply(KLabel('#Exists', [Sorts.INT, Sorts.BOOL]), [KVariable('X'), KApply('_==Int_', [KVariable('X'), KVariable('Y')])]), KVariable('Exists_8676e20c')),
+            (True, KApply(KLabel('#Ceil', [KSort('Set'), Sorts.GENERATED_TOP_CELL]), [KApply(KLabel('_Set_', [KVariable('_'), KVariable('_')]))]), KVariable('Ceil_37f1b5e5')),
+            (True, KApply(KLabel('#Not', [Sorts.GENERATED_TOP_CELL]), [KApply(KLabel('#Ceil', [KSort('Set'), Sorts.GENERATED_TOP_CELL]), [KApply(KLabel('_Set_', [KVariable('_'), KVariable('_')]))])]), KApply('notBool_', [KVariable('Ceil_37f1b5e5')])),
+            (True, KApply(KLabel('#Exists', [Sorts.INT, Sorts.BOOL]), [KVariable('X'), KApply('_==Int_', [KVariable('X'), KVariable('Y')])]), KVariable('Exists_6acf2557')),
         )
 
         for i, (unsafe, before, expected) in enumerate(test_data):
diff --git a/pyk/src/pyk/tests/test_kompile.py b/pyk/src/pyk/tests/test_kompile.py
index d1536a26242..4648056958d 100644
--- a/pyk/src/pyk/tests/test_kompile.py
+++ b/pyk/src/pyk/tests/test_kompile.py
@@ -15,8 +15,9 @@ def test_all_args(self):
             md_selector='k & ! nobytes & ! node',
             hook_namespaces=['JSON', 'KRYPTO', 'BLOCKCHAIN'],
             emit_json=True,
+            post_process='echo "hello"',
             concrete_rules=['foo', 'bar'],
-            additional_args=['--new-fangled-option', 'buzz']
+            additional_args=['--new-fangled-option', 'buzz'],
         )
         expected = [
             '--main-module', 'MAIN-MODULE',
@@ -28,6 +29,7 @@ def test_all_args(self):
             '--md-selector', 'k & ! nobytes & ! node',
             '--hook-namespaces', 'JSON KRYPTO BLOCKCHAIN',
             '--emit-json',
+            '--post-process', "'echo \"hello\"'",
             '--concrete-rules', 'foo,bar',
             '--new-fangled-option', 'buzz'
         ]
diff --git a/pyk/src/pyk/utils.py b/pyk/src/pyk/utils.py
index fdc95e3df68..a649be63138 100644
--- a/pyk/src/pyk/utils.py
+++ b/pyk/src/pyk/utils.py
@@ -64,6 +64,10 @@ def merge_with(f, d1: Mapping, d2: Mapping) -> Dict:
     return res
 
 
+def filter_none(mapping: Mapping[K, V]) -> Dict[K, V]:
+    return {k: v for k, v in mapping.items() if v is not None}
+
+
 def find_common_items(l1: Iterable[T], l2: Iterable[T]) -> Tuple[List[T], List[T], List[T]]:
     common = []
     for i in l1: