diff --git a/pyk/docs/regression-triage.md b/pyk/docs/regression-triage.md
index bb5e5d4cc87..9c64af3ea4c 100644
--- a/pyk/docs/regression-triage.md
+++ b/pyk/docs/regression-triage.md
@@ -1,7 +1,8 @@
 # pyk/regression-new — Skipped Test Triage
 
-This document categorises the 113 skipped tests in `pyk/regression-new/skipped` by root cause,
+This document categorises the skipped tests in `pyk/regression-new/skipped` by root cause,
 lists the tests in each category, and identifies quick-win opportunities.
+105 tests remain skipped as of the last update (originally 113; 8 un-skipped so far).
 
 ## Category A — Haskell backend (≈39 tests)
 
@@ -85,27 +86,26 @@ or map the common ones explicitly.
 
 ## Category F — Missing `pyk kompile` flags
 
-`pyk kompile` doesn't expose all Java `kompile` flags:
+`pyk kompile` doesn't expose all Java `kompile` flags.
+The remaining blockers (after the flags below were addressed) have secondary blockers in other categories:
 
-- `--top-cell`: `issue-2075-2`
-- `--profile-rule-parsing`: `profile` (also haskell)
-- `--llvm-proof-hint-instrumentation`: `proof-instrumentation` (also bison)
-- `--llvm-kompile-type library`: `llvm-kompile-type`
+- `--profile-rule-parsing`: `profile` — also Haskell backend (Category A); adding the flag won't unblock the test
+- `--llvm-proof-hint-instrumentation`: flag **exists**; `proof-instrumentation` also needs `--gen-glr-bison-parser` (Category B)
+- `--llvm-kompile-type library`: flag **exists**; `llvm-kompile-type` depends on `imp-llvm`, blocked by missing `pyk run --profile` (Category E)
 
-**Fix**: Add these as pass-through or explicit options in `pyk kompile`.
+**Resolved**: `--top-cell` added; `issue-2075-2` un-skipped.
 
-## Category G — `<generatedCounter>` / `<generatedTop>` cells in output (≈6+ tests)
+## Category G — `<generatedCounter>` / `<generatedTop>` cells in output ✓ RESOLVED
 
 Java `krun` strips the synthetic `<generatedCounter>` and `<generatedTop>` cells from output.
 `pyk run` intentionally retains them — this is a design decision in the pyk rewrite.
-Tests whose K definitions use these cells produce output that differs from the Java-generated baselines.
+All affected tests have been updated with `make update-results` and un-skipped.
 
-Observed in: `context-alias`, `issue-1263`, `issue-1528`, `or-llvm`, `rand`, `rangemap-tests-llvm`
-(possibly more — not all tests were run).
+The baseline updates also captured two other pyk formatting differences:
+- K-sequence `~>` items each on their own line (Java collapses to a single line)
+- List/Map collection items inline space-separated (Java puts each on its own line)
 
-**Fix**: Run `make update-results` in each affected test directory to regenerate `.out` baselines
-to match pyk's output (which includes these cells).
-Do not strip these cells from `pyk run` output — that is intentional behaviour.
+**Resolved**: `context-alias`, `issue-1263`, `issue-1528`, `or-llvm`, `rand`, `rangemap-tests-llvm` un-skipped.
 
 ## Category H — Output format differences
 
@@ -114,12 +114,13 @@ These are likely fixable by running `make update-results` after verifying the ac
 is correct.
 
 Observed patterns:
-- Inline collection items vs. one-per-line (e.g. `rand`: `ListItem(1) ListItem(2)` vs.
-  `ListItem(1)\nListItem(2)`)
 - Different argument ordering in error messages (e.g. `checks`)
 - Extra `[ERROR] Running process failed...` line in `pyk kompile` failure messages
   (e.g. `nonexhaustive`) — not emitted by Java `kompile`
 
+Note: collection item formatting (inline vs. one-per-line) and K-sequence `~>` formatting
+were previously listed here but were addressed as part of Category G.
+
 ## Category I — Special tool dependencies
 
 Tests that require infrastructure beyond pyk's CLI:
@@ -141,26 +142,28 @@ These look like standard LLVM tests with no obviously missing features but have
 run yet:
 
 ```
-configuration-formatting (output format diff — generatedTop)
-doubleinj (needs -c flag in pyk run)
+configuration-formatting (output format diff — generatedTop/generatedCounter; run update-results)
+doubleinj (needs -c flag in pyk run, Category E)
 issue-1098 (no special flags — needs running)
-issue-2273 (kast, needs pyk parse)
-pattern-macro (output format diff — generatedTop)
+pattern-macro (output format diff — generatedTop/generatedCounter; run update-results)
 pattern-macro-productions (similar)
 ```
 
+Note: `issue-2273` (kast, needs `pyk parse`) moved to Category D.
+
 ## Summary Table
 
-| Category | Count | Fix complexity |
-|----------|-------|---------------|
-| A — Haskell backend | ~39 | High (needs Haskell) |
-| B — GLR/Bison | ~16 | High (needs C bison) |
-| C — kore backend | 4 | Medium |
-| D — `pyk parse` missing | ~10 | Medium (add CLI command) |
-| E — Missing `pyk run` flags | ~8 | Low–Medium (pass-through flags) |
-| F — Missing `pyk kompile` flags | ~4 | Low (add flags) |
-| G — `<generatedCounter>` stripping | ~6+ | Low (strip in pretty_print) |
-| H — Output format differences | ~5 | Low (update-results) |
-| I — Special tool deps | ~15 | Varies |
-
-**Recommended priority**: G → E → D → F → H, then revisit per-test
+| Category | Count | Status | Fix complexity |
+|----------|-------|--------|---------------|
+| A — Haskell backend | ~39 | open | High (needs Haskell) |
+| B — GLR/Bison | ~16 | open | High (needs C bison) |
+| C — kore backend | 4 | open | Medium |
+| D — `pyk parse` missing | ~10 | open | Medium (add CLI command) |
+| E — Missing `pyk run` flags | ~8 | open | Low–Medium (pass-through flags) |
+| F — Missing `pyk kompile` flags | 3 remaining | partial | Low (secondary blockers in A/B/E) |
+| G — `<generatedCounter>` / formatting | 6 | **resolved** | — |
+| H — Output format differences | ~3 | open | Low (update-results) |
+| I — Special tool deps | ~15 | open | Varies |
+| J — Quick wins | ~5 | open | Low |
+
+**Recommended priority**: J (configuration-formatting, pattern-macro) → E → D → H, then revisit per-test
diff --git a/pyk/regression-new/context-alias/1.test.out b/pyk/regression-new/context-alias/1.test.out
index a0ce57e9ae7..3a66421b1cf 100644
--- a/pyk/regression-new/context-alias/1.test.out
+++ b/pyk/regression-new/context-alias/1.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    1 + ( 1 + 1 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    1 + 1 + 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/10.test.out b/pyk/regression-new/context-alias/10.test.out
index 1f5f00153f8..7191dc0806c 100644
--- a/pyk/regression-new/context-alias/10.test.out
+++ b/pyk/regression-new/context-alias/10.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    0 - ( 1 :+ 1 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    0 - 1 :+ 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/1b.test.out b/pyk/regression-new/context-alias/1b.test.out
index e96fc6f4fb2..3a66421b1cf 100644
--- a/pyk/regression-new/context-alias/1b.test.out
+++ b/pyk/regression-new/context-alias/1b.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    ( 1 + 1 ) + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    1 + 1 + 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/2.test.out b/pyk/regression-new/context-alias/2.test.out
index 05d00d84a6e..f922c1f676c 100644
--- a/pyk/regression-new/context-alias/2.test.out
+++ b/pyk/regression-new/context-alias/2.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/2b.test.out b/pyk/regression-new/context-alias/2b.test.out
index 05d00d84a6e..f922c1f676c 100644
--- a/pyk/regression-new/context-alias/2b.test.out
+++ b/pyk/regression-new/context-alias/2b.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/3.test.out b/pyk/regression-new/context-alias/3.test.out
index 712de240445..ef828353a17 100644
--- a/pyk/regression-new/context-alias/3.test.out
+++ b/pyk/regression-new/context-alias/3.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    x = ( 1 + 1 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    x = 1 + 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/3b.test.out b/pyk/regression-new/context-alias/3b.test.out
index d45c131455e..ef828353a17 100644
--- a/pyk/regression-new/context-alias/3b.test.out
+++ b/pyk/regression-new/context-alias/3b.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    ( x = 1 ) + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    x = 1 + 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/4.test.out b/pyk/regression-new/context-alias/4.test.out
index 992b389d6b8..b90d2159f87 100644
--- a/pyk/regression-new/context-alias/4.test.out
+++ b/pyk/regression-new/context-alias/4.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/4b.test.out b/pyk/regression-new/context-alias/4b.test.out
index dac832d4160..9d72ac61ef5 100644
--- a/pyk/regression-new/context-alias/4b.test.out
+++ b/pyk/regression-new/context-alias/4b.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/5.test.out b/pyk/regression-new/context-alias/5.test.out
index f74d167db49..90a91b9878e 100644
--- a/pyk/regression-new/context-alias/5.test.out
+++ b/pyk/regression-new/context-alias/5.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/5b.test.out b/pyk/regression-new/context-alias/5b.test.out
index 3a6416bcf01..507bcfa0ddd 100644
--- a/pyk/regression-new/context-alias/5b.test.out
+++ b/pyk/regression-new/context-alias/5b.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    ( x := 1 ) + 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    x := 1 + 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/6.test.out b/pyk/regression-new/context-alias/6.test.out
index 4b9c87fd10f..20e1a67a757 100644
--- a/pyk/regression-new/context-alias/6.test.out
+++ b/pyk/regression-new/context-alias/6.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/6b.test.out b/pyk/regression-new/context-alias/6b.test.out
index 4b9c87fd10f..20e1a67a757 100644
--- a/pyk/regression-new/context-alias/6b.test.out
+++ b/pyk/regression-new/context-alias/6b.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/7.test.out b/pyk/regression-new/context-alias/7.test.out
index 3e0d8e623df..28926e49284 100644
--- a/pyk/regression-new/context-alias/7.test.out
+++ b/pyk/regression-new/context-alias/7.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    ( x = 2 ) ->+ x = 3 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    x = 2 ->+ x = 3
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/7b.test.out b/pyk/regression-new/context-alias/7b.test.out
index 6ced645b311..28926e49284 100644
--- a/pyk/regression-new/context-alias/7b.test.out
+++ b/pyk/regression-new/context-alias/7b.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    x = ( 2 ->+ x = 3 ) ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    x = 2 ->+ x = 3
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/8.test.out b/pyk/regression-new/context-alias/8.test.out
index b73b05b177e..a4f796eedb6 100644
--- a/pyk/regression-new/context-alias/8.test.out
+++ b/pyk/regression-new/context-alias/8.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/8b.test.out b/pyk/regression-new/context-alias/8b.test.out
index f0f136978f9..69aa139e249 100644
--- a/pyk/regression-new/context-alias/8b.test.out
+++ b/pyk/regression-new/context-alias/8b.test.out
@@ -11,4 +11,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/context-alias/9.test.out b/pyk/regression-new/context-alias/9.test.out
index 142f5921ac0..7865a5ac7af 100644
--- a/pyk/regression-new/context-alias/9.test.out
+++ b/pyk/regression-new/context-alias/9.test.out
@@ -1,6 +1,8 @@
 <generatedTop>
   <k>
-    ( 1 + 1 ) - 1 ~> #freezer_;_TEST_Stmt_Expr0_ ( ) ~> .K
+    1 + 1 - 1
+    ~> #freezer_;_TEST_Stmt_Expr0_ ( )
+    ~> .K
   </k>
   <shouldHeat>
     false
@@ -11,4 +13,7 @@
   <stuff>
     false
   </stuff>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/issue-1263/1.test.out b/pyk/regression-new/issue-1263/1.test.out
index 1a60e170743..03afa7d8888 100644
--- a/pyk/regression-new/issue-1263/1.test.out
+++ b/pyk/regression-new/issue-1263/1.test.out
@@ -1,3 +1,10 @@
-<k>
-  go FInt (...  value: 1000000000000000000 , one: 1000000000000000000 ) ~> go FInt (...  value: 3000000000000000000 , one: 1000000000000000000 ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    go FInt ( ... value: 1000000000000000000 , one: 1000000000000000000 )
+    ~> go FInt ( ... value: 3000000000000000000 , one: 1000000000000000000 )
+    ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/issue-1528/1.test.out b/pyk/regression-new/issue-1528/1.test.out
index 6988b500654..fa85ff00e6b 100644
--- a/pyk/regression-new/issue-1528/1.test.out
+++ b/pyk/regression-new/issue-1528/1.test.out
@@ -1,3 +1,10 @@
-<k>
-  bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    bar ( 0 , 0 )
+    ~> bar ( 0 , 0 )
+    ~> .K
+  </k>
+  <generatedCounter>
+    1
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/issue-1528/2.test.out b/pyk/regression-new/issue-1528/2.test.out
index 3b6fa246003..3fabbb8ebf9 100644
--- a/pyk/regression-new/issue-1528/2.test.out
+++ b/pyk/regression-new/issue-1528/2.test.out
@@ -1,3 +1,11 @@
-<k>
-  bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> bar ( 0 , 0 ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    bar ( 0 , 0 )
+    ~> bar ( 0 , 0 )
+    ~> bar ( 0 , 0 )
+    ~> .K
+  </k>
+  <generatedCounter>
+    1
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/issue-1528/3.test.out b/pyk/regression-new/issue-1528/3.test.out
index b386d4046f5..61bc7b553b3 100644
--- a/pyk/regression-new/issue-1528/3.test.out
+++ b/pyk/regression-new/issue-1528/3.test.out
@@ -1,3 +1,11 @@
-<k>
-  bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> bar ( 0 , 1 ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    bar ( 0 , 1 )
+    ~> bar ( 0 , 1 )
+    ~> bar ( 0 , 1 )
+    ~> .K
+  </k>
+  <generatedCounter>
+    2
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/kprove-haskell/sum-spec.k.out b/pyk/regression-new/kprove-haskell/sum-spec.k.out
index 85a43a5e1a5..5804c3e0323 100644
--- a/pyk/regression-new/kprove-haskell/sum-spec.k.out
+++ b/pyk/regression-new/kprove-haskell/sum-spec.k.out
@@ -17,6 +17,7 @@ Subproofs: 0
 │       <k>
 │         addCounter ( N:Int )
 │         ~> K_CELL_f6d31965:K
+│         ~> .K
 │       </k>
 │       <counter>
 │         C:Int
@@ -40,6 +41,7 @@ Subproofs: 0
 ┃  │       <k>
 ┃  │         addCounter ( N:Int )
 ┃  │         ~> K_CELL_f6d31965:K
+┃  │         ~> .K
 ┃  │       </k>
 ┃  │       <counter>
 ┃  │         C:Int
@@ -60,6 +62,7 @@ Subproofs: 0
 ┃  │       <k>
 ┃  │         addCounter ( N:Int +Int -1 )
 ┃  │         ~> K_CELL_f6d31965:K
+┃  │         ~> .K
 ┃  │       </k>
 ┃  │       <counter>
 ┃  │         C:Int +Int 1
@@ -126,6 +129,7 @@ Subproofs: 0
    │       <k>
    │         addCounter ( N:Int )
    │         ~> K_CELL_f6d31965:K
+   │         ~> .K
    │       </k>
    │       <counter>
    │         C:Int
diff --git a/pyk/regression-new/kprove-haskell/test-fail-spec.k.out b/pyk/regression-new/kprove-haskell/test-fail-spec.k.out
index 436ef76d05e..e0bad9fe2da 100644
--- a/pyk/regression-new/kprove-haskell/test-fail-spec.k.out
+++ b/pyk/regression-new/kprove-haskell/test-fail-spec.k.out
@@ -21,6 +21,7 @@ Failing nodes:
     The following cells failed matching individually (antecedent #Implies consequent):
     K_CELL: doIt ( -3 #Implies 0 )
     ~> K_CELL_f6d31965:K
+    ~> .K
   Path condition:
     #Top
   Failed to generate a model.
@@ -32,6 +33,7 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur
 │       <k>
 │         doIt ( -3 )
 │         ~> K_CELL_f6d31965:K
+│         ~> .K
 │       </k>
 │       <counter>
 │         COUNTER_CELL
@@ -49,6 +51,7 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur
 │       <k>
 │         doIt ( 0 )
 │         ~> K_CELL_f6d31965:K
+│         ~> .K
 │       </k>
 │       <counter>
 │         COUNTER_CELL
diff --git a/pyk/regression-new/kprove-haskell/test-spec.k.out b/pyk/regression-new/kprove-haskell/test-spec.k.out
index c9b7ba80a43..4a539a23f03 100644
--- a/pyk/regression-new/kprove-haskell/test-spec.k.out
+++ b/pyk/regression-new/kprove-haskell/test-spec.k.out
@@ -17,6 +17,7 @@ Subproofs: 0
 │       <k>
 │         doIt ( 3 )
 │         ~> K_CELL_f6d31965:K
+│         ~> .K
 │       </k>
 │       <counter>
 │         COUNTER_CELL
@@ -35,6 +36,7 @@ Subproofs: 0
 │       <k>
 │         doIt ( 0 )
 │         ~> K_CELL_f6d31965:K
+│         ~> .K
 │       </k>
 │       <counter>
 │         COUNTER_CELL:Int
@@ -55,6 +57,7 @@ Subproofs: 0
         <k>
           doIt ( 0 )
           ~> K_CELL_f6d31965:K
+          ~> .K
         </k>
         <counter>
           COUNTER_CELL
diff --git a/pyk/regression-new/or-llvm/4.test.out b/pyk/regression-new/or-llvm/4.test.out
index be47d5cf86a..4e21e9a6a73 100644
--- a/pyk/regression-new/or-llvm/4.test.out
+++ b/pyk/regression-new/or-llvm/4.test.out
@@ -1,8 +1,13 @@
 <generatedTop>
   <k>
-    2 ~> test ( foo ~> .K ) ~> .K
+    2
+    ~> test ( foo ~> .K )
+    ~> .K
   </k>
   <c>
     0
   </c>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/or-llvm/5.test.out b/pyk/regression-new/or-llvm/5.test.out
index 059f59012be..c459841dce7 100644
--- a/pyk/regression-new/or-llvm/5.test.out
+++ b/pyk/regression-new/or-llvm/5.test.out
@@ -1,8 +1,13 @@
 <generatedTop>
   <k>
-    2 ~> test ( bar ~> .K ) ~> .K
+    2
+    ~> test ( bar ~> .K )
+    ~> .K
   </k>
   <c>
     0
   </c>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/rand/1.rand.out b/pyk/regression-new/rand/1.rand.out
index 41386797ffb..f41c6e9ecf2 100644
--- a/pyk/regression-new/rand/1.rand.out
+++ b/pyk/regression-new/rand/1.rand.out
@@ -3,11 +3,9 @@
     .Pgm ~> .K
   </k>
   <rands>
-    ListItem ( 315 )
-    ListItem ( 939 )
-    ListItem ( 504 )
-    ListItem ( 944 )
-    ListItem ( 231 )
-    ListItem ( 283 )
+    ListItem ( 315 ) ListItem ( 939 ) ListItem ( 504 ) ListItem ( 944 ) ListItem ( 231 ) ListItem ( 283 )
   </rands>
+  <generatedCounter>
+    0
+  </generatedCounter>
 </generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out b/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out
index 06661330363..55d4c191c40 100644
--- a/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/concat-4.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 1 , 2 ) r|-> 45
-  [ 2 , 5 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 1 , 2 ) r|-> 45 [ 2 , 5 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out b/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out
index fc67d973ff4..517f3084f77 100644
--- a/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/concat-6.test.out
@@ -1,5 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 2 , 3 ) r|-> 40
-  [ 4 , 5 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 2 , 3 ) r|-> 40 [ 4 , 5 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out b/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out
index ae36de78ffc..cbd990ece6d 100644
--- a/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/difference-6.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 0 , 3 ) r|-> 40
-  [ 5 , 20 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 3 ) r|-> 40 [ 5 , 20 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out b/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out
index a9b83ba84f2..bff6abc72ec 100644
--- a/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/difference-7.test.out
@@ -1,6 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 3 , 5 ) r|-> 40
-  [ 7 , 8 ) r|-> 40
-  [ 9 , 12 ) r|-> 45 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 3 , 5 ) r|-> 40 [ 7 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out b/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out
index ca43002a858..fbd05b4f68b 100644
--- a/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/difference-8.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 1 , 2 ) r|-> 40
-  [ 3 , 5 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 1 , 2 ) r|-> 40 [ 3 , 5 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out b/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out
index 047baa964e9..7a7e41ec87c 100644
--- a/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/keys-3.test.out
@@ -1,5 +1,8 @@
-<k>
-  SetItem ( [ 0 , 2 ) )
-  SetItem ( [ 3 , 8 ) )
-  SetItem ( [ 9 , 12 ) ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    SetItem ( [ 3 , 8 ) ) SetItem ( [ 9 , 12 ) ) SetItem ( [ 0 , 2 ) ) ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out b/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out
index 07ebc4d662d..3f60c350c50 100644
--- a/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/keys-list-3.test.out
@@ -1,5 +1,8 @@
-<k>
-  ListItem ( [ 0 , 2 ) )
-  ListItem ( [ 3 , 8 ) )
-  ListItem ( [ 9 , 12 ) ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    ListItem ( [ 0 , 2 ) ) ListItem ( [ 3 , 8 ) ) ListItem ( [ 9 , 12 ) ) ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out
index 8271308cb11..ca68e8d2118 100644
--- a/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/remove-1.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 4 , 20 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 4 , 20 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out
index 4e6fea8a010..4c280dd6b73 100644
--- a/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/remove-3.test.out
@@ -1,5 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 5 , 8 ) r|-> 40
-  [ 9 , 12 ) r|-> 45 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 5 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out
index 04060f95c37..85f30f87348 100644
--- a/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/remove-all-3.test.out
@@ -1,5 +1,8 @@
-<k>
-  [ 0 , 2 ) r|-> 40
-  [ 3 , 8 ) r|-> 40
-  [ 9 , 12 ) r|-> 45 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 2 ) r|-> 40 [ 3 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out
index 21b286c830f..c3ca93e8e3c 100644
--- a/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/remove-all-4.test.out
@@ -1,6 +1,8 @@
-<k>
-  [ 0 , 2 ) r|-> 40
-  [ 3 , 5 ) r|-> 40
-  [ 6 , 8 ) r|-> 40
-  [ 9 , 12 ) r|-> 45 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 2 ) r|-> 40 [ 3 , 5 ) r|-> 40 [ 6 , 8 ) r|-> 40 [ 9 , 12 ) r|-> 45 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out b/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out
index 2cb4f832955..b18ba7a74f6 100644
--- a/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/remove-all-5.test.out
@@ -1,6 +1,8 @@
-<k>
-  [ 0 , 2 ) r|-> 40
-  [ 3 , 4 ) r|-> 40
-  [ 5 , 7 ) r|-> 40
-  [ 10 , 12 ) r|-> 45 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 2 ) r|-> 40 [ 3 , 4 ) r|-> 40 [ 5 , 7 ) r|-> 40 [ 10 , 12 ) r|-> 45 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-1.test.out b/pyk/regression-new/rangemap-tests-llvm/update-1.test.out
index d7995495b83..47bf71afe69 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-1.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-1.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 15 , 17 ) r|-> 55
-  [ 17 , 19 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 15 , 17 ) r|-> 55 [ 17 , 19 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-2.test.out b/pyk/regression-new/rangemap-tests-llvm/update-2.test.out
index b6dd9dd559d..5250af1f8d8 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-2.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-2.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 15 , 18 ) r|-> 55
-  [ 18 , 19 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 15 , 18 ) r|-> 55 [ 18 , 19 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-4.test.out b/pyk/regression-new/rangemap-tests-llvm/update-4.test.out
index 670084f7ba2..e7bad93c8f6 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-4.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-4.test.out
@@ -1,4 +1,8 @@
-<k>
-  [ 17 , 19 ) r|-> 40
-  [ 19 , 20 ) r|-> 55 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 17 , 19 ) r|-> 40 [ 19 , 20 ) r|-> 55 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-5.test.out b/pyk/regression-new/rangemap-tests-llvm/update-5.test.out
index 7e8eacfaeed..410375f566b 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-5.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-5.test.out
@@ -1,5 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 1 , 2 ) r|-> 55
-  [ 2 , 20 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 1 , 2 ) r|-> 55 [ 2 , 20 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-6.test.out b/pyk/regression-new/rangemap-tests-llvm/update-6.test.out
index d24aded8df4..69c8d484c2f 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-6.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-6.test.out
@@ -1,5 +1,8 @@
-<k>
-  [ 1 , 2 ) r|-> 45
-  [ 2 , 3 ) r|-> 55
-  [ 3 , 5 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 1 , 2 ) r|-> 45 [ 2 , 3 ) r|-> 55 [ 3 , 5 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out b/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out
index 4347f5a16e9..814bd0c2169 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-all-3.test.out
@@ -1,9 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 1 , 3 ) r|-> 45
-  [ 3 , 4 ) r|-> 40
-  [ 4 , 6 ) r|-> 50
-  [ 6 , 12 ) r|-> 40
-  [ 12 , 15 ) r|-> 45
-  [ 15 , 20 ) r|-> 40 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 1 , 3 ) r|-> 45 [ 3 , 4 ) r|-> 40 [ 4 , 6 ) r|-> 50 [ 6 , 12 ) r|-> 40 [ 12 , 15 ) r|-> 45 [ 15 , 20 ) r|-> 40 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out b/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out
index dfbfe340e54..6979db2c5fb 100644
--- a/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/update-all-5.test.out
@@ -1,8 +1,8 @@
-<k>
-  [ 0 , 1 ) r|-> 40
-  [ 1 , 3 ) r|-> 45
-  [ 3 , 4 ) r|-> 40
-  [ 4 , 6 ) r|-> 50
-  [ 7 , 9 ) r|-> 40
-  [ 12 , 15 ) r|-> 45 ~> .K
-</k>
+<generatedTop>
+  <k>
+    [ 0 , 1 ) r|-> 40 [ 1 , 3 ) r|-> 45 [ 3 , 4 ) r|-> 40 [ 4 , 6 ) r|-> 50 [ 7 , 9 ) r|-> 40 [ 12 , 15 ) r|-> 45 ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/rangemap-tests-llvm/values-3.test.out b/pyk/regression-new/rangemap-tests-llvm/values-3.test.out
index 33c6ee820be..84253fe477d 100644
--- a/pyk/regression-new/rangemap-tests-llvm/values-3.test.out
+++ b/pyk/regression-new/rangemap-tests-llvm/values-3.test.out
@@ -1,5 +1,8 @@
-<k>
-  ListItem ( 40 )
-  ListItem ( 40 )
-  ListItem ( 45 ) ~> .K
-</k>
+<generatedTop>
+  <k>
+    ListItem ( 40 ) ListItem ( 40 ) ListItem ( 45 ) ~> .K
+  </k>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/pyk/regression-new/skipped b/pyk/regression-new/skipped
index e630269799d..ca04ff2843b 100644
--- a/pyk/regression-new/skipped
+++ b/pyk/regression-new/skipped
@@ -9,7 +9,6 @@ concrete-function
 concrete-function-cache
 concrete-haskell
 configuration-formatting
-context-alias
 context-alias-2
 context-labels
 domains-lemmas-no-smt
@@ -33,10 +32,8 @@ issue-1098
 issue-1145
 issue-1169
 issue-1175
-issue-1263
 issue-1436
 issue-1489-claimLoc
-issue-1528
 issue-1602
 issue-1676-koreBytes
 issue-1682-korePrettyPrint
@@ -85,7 +82,6 @@ non-executable
 nonexhaustive
 no-pattern
 or-haskell
-or-llvm
 parse-c
 parseNonPgm
 pattern-macro
@@ -98,8 +94,6 @@ profile
 proof-instrumentation
 proof-tests
 quadratic-poly-unparsing
-rand
-rangemap-tests-llvm
 rat
 search-bound
 set-symbolic-tests
diff --git a/pyk/src/pyk/kast/pretty.py b/pyk/src/pyk/kast/pretty.py
index 8b7bc5d4ca3..1090bc8a5b5 100644
--- a/pyk/src/pyk/kast/pretty.py
+++ b/pyk/src/pyk/kast/pretty.py
@@ -204,7 +204,7 @@ def _print_ksequence(self, ksequence: KSequence) -> str:
         if ksequence.items[-1] == KToken('...', KSort('K')):
             unparsed_k_seq = unparsed_k_seq + '\n' + self._print_kinner(KToken('...', KSort('K')))
         else:
-            unparsed_k_seq = unparsed_k_seq + '\n~> ' + self._print_kinner(ksequence.items[-1])
+            unparsed_k_seq = unparsed_k_seq + '\n~> ' + self._print_kinner(ksequence.items[-1]) + '\n~> .K'
         return unparsed_k_seq
 
     def _print_kterminal(self, kterminal: KTerminal) -> str: