From f5566e377ffa1edcc20f8471591a8cda2a6d37f1 Mon Sep 17 00:00:00 2001
From: Musab Alturki <42160792+malturki@users.noreply.github.com>
Date: Tue, 29 Sep 2026 14:05:55 +0000
Subject: [PATCH] Preserve symbolic List frames in matcher residuals

---
 kore/src/Kore/Rewrite/Axiom/Matcher.hs       |  3 +--
 kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs | 10 ++++++++++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/kore/src/Kore/Rewrite/Axiom/Matcher.hs b/kore/src/Kore/Rewrite/Axiom/Matcher.hs
index 5599874bce..9d054f1af0 100644
--- a/kore/src/Kore/Rewrite/Axiom/Matcher.hs
+++ b/kore/src/Kore/Rewrite/Axiom/Matcher.hs
@@ -24,7 +24,6 @@ import Data.PQueue.Min (
     MinQueue,
  )
 import Data.PQueue.Min qualified as MinQueue
-import Data.Sequence (Seq ((:|>)))
 import Data.Sequence qualified as Seq
 import Data.Set (
     Set,
@@ -445,7 +444,7 @@ patternMatch' sideCondition ((MatchItem pat subject boundVars boundSet) : rest)
                                     then
                                         let (start, l2') = Seq.splitAt (length l1) l2
                                          in decomposeList $
-                                                (var1, List.asInternal tools sort (l2' :|> var2))
+                                                (var1, mkApplySymbol symbol1 [List.asInternal tools sort l2', var2])
                                                     : zip (toList l1) (toList start)
                                     else failMatch "subject list is too short"
                     (App_ symbol1 children1, App_ symbol2 children2) ->
diff --git a/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs b/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs
index ab3342bc22..aeb0a757d8 100644
--- a/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs
+++ b/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs
@@ -815,6 +815,16 @@ test_matching_List =
         [ (inject xInt, two)
         , (yList, mkList [one])
         ]
+    , matches
+        "framed-list pattern preserves nonempty subject prefix"
+        (prefixList [one] xList)
+        (prefixList [one, two] yList)
+        [(xList, prefixList [two] yList)]
+    , matches
+        "framed-list pattern preserves empty subject prefix"
+        (prefixList [one] xList)
+        (prefixList [one] yList)
+        [(xList, prefixList [] yList)]
     ]
   where
     xList = inject $ configElementVariableFromId (testId "xList") Mock.listSort