diff --git a/docs/2022-07-18-JSON-RPC-Server-API.md b/docs/2022-07-18-JSON-RPC-Server-API.md
index 6f5e2b5ac0..8678725b7f 100644
--- a/docs/2022-07-18-JSON-RPC-Server-API.md
+++ b/docs/2022-07-18-JSON-RPC-Server-API.md
@@ -142,7 +142,25 @@ This response has no additional fields.
 
 ##### `"reason": "aborted"`
 Execution reached a state that the server cannot handle.
-This response has no additional fields.
+The `unknown-predicate` field MAY contain a predicate that could not be decided by the server's constraint solver.
+
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "result": {
+    "state": {
+      "term": {"format":"KORE", "version":1, "term":{}},
+      "predicate": {"format":"KORE", "version":1, "term":{}},
+      "substitution": {"format":"KORE", "version":1, "term":{}},
+    },
+    "depth": 2,
+    "reason": "aborted",
+    "unknown-predicate": {"format":"KORE", "version":1, "term":{}}
+    "logs": []
+  }
+}
+```
 
 ##### `"reason": "cut-point-rule"`
 Execution was about to perform a rewrite with a rule whose label is one of the `cut-point-rules` labels/IDs of the request.  
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
index 73809a59c4..81340a5460 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs
@@ -134,6 +134,7 @@ data ExecuteResult = ExecuteResult
     , nextStates :: Maybe [ExecuteState]
     , rule :: Maybe Text
     , logs :: Maybe [LogEntry]
+    , unknownPredicate :: Maybe KoreJson
     }
     deriving stock (Generic, Show, Eq)
     deriving
diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs
index fc59af03d7..b08d24209c 100644
--- a/kore/src/Kore/JsonRpc.hs
+++ b/kore/src/Kore/JsonRpc.hs
@@ -226,6 +226,7 @@ respond serverState moduleName runSMT =
                                         , rule = Nothing
                                         , nextStates = Nothing
                                         , logs = mkLogs mbDuration rules
+                                        , unknownPredicate = Nothing
                                         }
                     GraphTraversal.GotStuck
                         _n
@@ -241,6 +242,7 @@ respond serverState moduleName runSMT =
                                         , rule = Nothing
                                         , nextStates = Nothing
                                         , logs = mkLogs mbDuration rules
+                                        , unknownPredicate = Nothing
                                         }
                     GraphTraversal.GotStuck
                         _n
@@ -256,6 +258,7 @@ respond serverState moduleName runSMT =
                                         , rule = Nothing
                                         , nextStates = Nothing
                                         , logs = mkLogs mbDuration rules
+                                        , unknownPredicate = Nothing
                                         }
                     GraphTraversal.Stopped
                         [Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules}]
@@ -271,6 +274,7 @@ respond serverState moduleName runSMT =
                                             , nextStates =
                                                 Just $ map (patternToExecState sort . Exec.rpcProgState) nexts
                                             , logs = mkLogs mbDuration rules
+                                            , unknownPredicate = Nothing
                                             }
                             | Just rule <- containsLabelOrRuleId rules terminalRules ->
                                 Right $
@@ -282,6 +286,7 @@ respond serverState moduleName runSMT =
                                             , rule
                                             , nextStates = Nothing
                                             , logs = mkLogs mbDuration rules
+                                            , unknownPredicate = Nothing
                                             }
                             | otherwise ->
                                 Right $
@@ -294,6 +299,7 @@ respond serverState moduleName runSMT =
                                             , nextStates =
                                                 Just $ map (patternToExecState sort . Exec.rpcProgState) nexts
                                             , logs = mkLogs mbDuration rules
+                                            , unknownPredicate = Nothing
                                             }
                     GraphTraversal.TimedOut
                         Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules}
@@ -307,6 +313,7 @@ respond serverState moduleName runSMT =
                                         , rule = Nothing
                                         , nextStates = Nothing
                                         , logs = mkLogs mbDuration rules
+                                        , unknownPredicate = Nothing
                                         }
                     -- these are programmer errors
                     result@GraphTraversal.Aborted{} ->