Claims are pre-processed, we might not always want this

[amelieled]

With the semantics (simplify-test.k):

module AND-SYNTAX
  imports BOOL

  syntax Bool ::= Bool "func-and" Bool [left, function, functional]
                | "(" Bool ")"         [bracket]

endmodule

module SIMPLIFY-TEST
  imports AND-SYNTAX

  rule true  func-and true  => true
  rule true  func-and false => false
  rule false func-and true  => false
  rule false func-and false => false

endmodule

and the KProver claim (simpl-func.k):

requires "simplify-test.k"
requires "domains.md"

module SIMPL-FUNC
    imports SIMPLIFY-TEST

    claim <k> ( true func-and false ) func-and (true func-and true) => false ... </k>

endmodule

I obtained, with the following command: ~$ KORE_EXEC_OPTS='--trace-rewrites simpl-func.yaml' kprove simpl-func.k

kore-exec: [290924] Warning (WarnTrivialClaim):
    Claim proven without rewriting at: ~/simpl-func.k:7:11-7:86
#Top

This warning is expected but the obtained claim in the file simpl-func.yaml has the shape phi -> wAF phi where phi = <k> false ~> . </k>. So, the claim in the YAML file isn't the user one.

~$ kompile --version

K version:    5.4.14
Build date:   Mon Oct 03 17:33:43 CEST 2022

[ana-pantilie]

The claim is proven immediately (without taking any rewrite steps) because the LHS is bottom. I'm not sure what you expected to happen.

[goodlyrottenapple]

There seem to be two issues here:

1. function-and being a function, we are not rewriting but the tracing only logs rewrite steps. The example could be modified to use a custom type instead of bool and not use the function attribute, so that function-and rules are rewrites
2. All claims are simplified before attempting all rewrites, printing the un-simplified/original claim would need some re-engineering

Can you let us know, which one was intended?

[amelieled]

Hi @ana-pantilie and @goodlyrottenapple ! Thanks for your answer. Indeed, the trace says that the claim is false ~> . => wAF false ~> . , but this is not the initial claim. For me, this is the main problem because the information generated by the trace is not true.

@ana-pantilie , I don't understand why the LHS is bottom.

[ana-pantilie]

@amelieled Please provide the actual trace (the yaml file), there isn't any provided in the issue.

[amelieled]

Hi @ana-pantilie This is the trace:

---
claim-id: null
claim: '/* Spa */ \implies{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}(
  /* D Sfa */ \top{SortGeneratedTopCell{}}(), /* Fl Fn D Spa */ Lbl''-LT-''generatedTop''-GT-''{}(
  /* Fl Fn D Spa */ Lbl''-LT-''k''-GT-''{}( /* Fl Fn D Spa */ kseq{}( /* Fl Fn D Sfa
  Cli */ /* Inj: */ inj{SortBool{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false")
  ), /* Fl Fn D Sfa */ Var''Unds''DotVar1:SortK{} ) ), /* Fl Fn D Spa */ Lbl''-LT-''generatedCounter''-GT-''{}(
  /* Fl Fn D Sfa */ Var''Unds''DotVar2:SortInt{} ) ) ), /* Spa */ weakAlwaysFinally{SortGeneratedTopCell{}}(
  /* Fl Fn D Spa */ Lbl''-LT-''generatedTop''-GT-''{}( /* Fl Fn D Spa */ Lbl''-LT-''k''-GT-''{}(
  /* Fl Fn D Spa */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortKItem{}}(
  /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa */ Var''Unds''DotVar1:SortK{}
  ) ), /* Fl Fn D Spa */ Lbl''-LT-''generatedCounter''-GT-''{}( /* Fl Fn D Sfa */
  Var''Unds''DotVar2:SortInt{} ) ) ) )'
task: reachability
steps:

[ana-pantilie]

Somewhat related: https://runtimeverification.slack.com/archives/C7E701MFG/p1668449003980349?thread_ts=1668188797.949799&cid=C7E701MFG

[ana-pantilie]

We should run the following experiment: remove https://github.com/runtimeverification/haskell-backend/blob/78738f36f7e56a637b2217808a188313c3ffc3a2/kore/src/Kore/Exec.hs#L1016 and see what breaks (test with relevant semantics).

[alexd1971]

We should run the following experiment: remove

https://github.com/runtimeverification/haskell-backend/blob/78738f36f7e56a637b2217808a188313c3ffc3a2/kore/src/Kore/Exec.hs#L1016

and see what breaks (test with relevant semantics).

I replaced this line with:

let claims = concat simplifiedSpecClaims

I guess this is what was supposed to be. And I got the following trace:

---
claim-id: null
claim: '/* Spa */ \implies{SortGeneratedTopCell{}}( /* Spa */ \and{SortGeneratedTopCell{}}(
  /* D Sfa */ \top{SortGeneratedTopCell{}}(), /* Fl Fn D Sfa */ Lbl''-LT-''generatedTop''-GT-''{}(
  /* Fl Fn D Sfa */ Lbl''-LT-''k''-GT-''{}( /* Fl Fn D Sfa */ kseq{}( /* Fl Fn D Sfa
  Cli */ /* Inj: */ inj{SortBool{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false")
  ), /* Fl Fn D Sfa */ Var''Unds''DotVar1:SortK{} ) ), /* Fl Fn D Sfa */ Lbl''-LT-''generatedCounter''-GT-''{}(
  /* Created: Kore.Rewrite.Rule.Expand.maybeNewVariable */ /* Fl Fn D Sfa */ Var''Unds''DotVar2:SortInt{}
  ) ) ), /* Spa */ weakAlwaysFinally{SortGeneratedTopCell{}}( /* Fl Fn D Spa */ Lbl''-LT-''generatedTop''-GT-''{}(
  /* Fl Fn D Spa */ Lbl''-LT-''k''-GT-''{}( /* Fl Fn D Spa */ kseq{}( /* Fl Fn D Sfa
  Cli */ /* Inj: */ inj{SortBool{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false")
  ), /* Fl Fn D Sfa */ Var''Unds''DotVar1:SortK{} ) ), /* Fl Fn D Spa */ Lbl''-LT-''generatedCounter''-GT-''{}(
  /* Created: Kore.Rewrite.Rule.Expand.maybeNewVariable */ /* Fl Fn D Sfa */ Var''Unds''DotVar2:SortInt{}
  ) ) ) )'
task: reachability
steps:

[alexd1971]

Here is the call stack to the function emittig the warning:

Trace to WarnTrivialClai
CallStack (from -prof):
  Kore.Log.WarnTrivialClaim.pretty (src/Kore/Log/WarnTrivialClaim.hs:(32,5)-(45,13))
  Kore.Log.makeKoreLogger.prettyActualEntry (src/Kore/Log.hs:(276,5)-(314,113))
  Kore.Log.makeKoreLogger.render (src/Kore/Log.hs:(263,5)-(274,47))
  Kore.Log.makeKoreLogger (src/Kore/Log.hs:(257,1)-(318,47))
  Kore.Log.withMainLogger.logAction (src/Kore/Log.hs:(114,9)-(118,51))
  Colog.Core.Action.<>.\ (src/Colog/Core/Action.hs:127:64-85)
  Colog.Core.Action.<> (src/Colog/Core/Action.hs:127:5-85)
  Log.logEntry (src/Log.hs:(262,5)-(264,45))
  Log.logEntry (src/Log.hs:199:5-30)
  Kore.Simplify.Simplify.logEntry (src/Kore/Simplify/Simplify.hs:159:33-40)
  Kore.Log.WarnTrivialClaim.warnProvenClaimZeroDepth (src/Kore/Log/WarnTrivialClaim.hs:(68,1)-(69,64))
  Kore.Reachability.Prove.proveClaim (src/Kore/Reachability/Prove.hs:(328,1)-(441,2))
  Kore.Reachability.Prove.proveClaimsWorker.verifyWorker (src/Kore/Reachability/Prove.hs:(290,9)-(312,26))
  Kore.Reachability.Prove.proveClaimsWorker (src/Kore/Reachability/Prove.hs:(275,1)-(315,62))
  Kore.Reachability.Prove.proveClaims (src/Kore/Reachability/Prove.hs:(214,1)-(260,35))
  Kore.Simplify.Simplify.runSimplifier (src/Kore/Simplify/Simplify.hs:(171,1)-(174,68))
  Kore.Simplify.API.evalSimplifier (src/Kore/Simplify/API.hs:(171,1)-(173,32))
  Kore.Simplify.API.evalSimplifierProofs (src/Kore/Simplify/API.hs:(179,1)-(198,60))
  Kore.Exec.prove (src/Kore/Exec.hs:(694,1)-(734,2))
  SMT.runSMT.\ (src/SMT.hs:(524,75)-(527,40))
  Log.generalBracket (src/Log.hs:240:56-64)
  SMT.runSMT (src/SMT.hs:(523,1)-(527,40))
  GlobalMain.execute.withZ3 (app/share/GlobalMain.hs:(560,5)-(564,18))
  GlobalMain.clockSomethingIO (app/share/GlobalMain.hs:(443,1)-(460,76))
  GlobalMain.execute (app/share/GlobalMain.hs:(554,1)-(574,13))
  Main.koreProve (app/exec/Main.hs:(762,1)-(868,17))
  Main.mainDispatch.mainDispatchWorker (app/exec/Main.hs:(651,5)-(665,48))
  Main.mainDispatch (app/exec/Main.hs:(641,1)-(665,48))
  Log.catch (src/Log.hs:240:44-53)
  Kore.Log.SQLite.withLogSQLite (src/Kore/Log/SQLite.hs:(87,1)-(109,2))
  Kore.Log.withRewriteTraceLogger (src/Kore/Log.hs:(163,1)-(170,47))
  Kore.Log.withSmtSolverLogger (src/Kore/Log.hs:(151,1)-(159,51))
  Kore.Log.withMainLogger (src/Kore/Log.hs:(103,1)-(123,2))
  Kore.Log.withLogger (src/Kore/Log.hs:(89,1)-(96,70))
  Kore.Log.runKoreLog (src/Kore/Log.hs:(231,1)-(234,92))
  Main.mainWithOptions.\ (app/exec/Main.hs:(594,65)-(610,20))
  Kore.BugReport.withBugReport (src/Kore/BugReport.hs:(132,1)-(176,24))
  Main.mainWithOptions (app/exec/Main.hs:(589,1)-(639,74))
  Main.main (app/exec/Main.hs:(575,1)-(583,47))

Perhaps it'll be useful for further investigation

[alexd1971]

Investigation how this warning appears:

According call stack above function warnProvenClaimZeroDepth, which generates this warning, is called from proveClame function. If we look into proveClame we can see:

...
        traversalResult <-
            GraphTraversal.graphTraversal
                finalNodeType
                searchOrder
                breadthLimit
                transition
                (Limit.Limit maxCounterexamples)
                limitedStrategyList
                (ProofDepth 0, startGoal)
...
        case traversalResult of
           ...
            GraphTraversal.Ended results -> do
                let depths = map fst results
                    maxProofDepth = sconcat (ProofDepth 0 :| trace ("Depths: " <> show depths)  depths)
                infoProvenDepth maxProofDepth
                warnProvenClaimZeroDepth maxProofDepth goal
                pure $ Right ()

So we can see that warning can only appear in case of GraphTraversal.Ended result. And looking into warnProvenClaimZeroDepth function:

warnProvenClaimZeroDepth ::
    MonadLog log =>
    ProofDepth ->
    SomeClaim ->
    log ()
warnProvenClaimZeroDepth (ProofDepth depth) rule =
    when (depth == 0) $ logEntry (WarnProvenClaimZeroDepth rule)

we can see that warning appears only in case ProofDepth 0.

Going down to the graphTraversal function which builds the result with ProofDepth value we can see that the main magic is happen in worker function defined like:

        worker Seq.Empty = trace "Seq is Empty" $ Ended . reverse <$> gets (mapMaybe extractState)
        worker (a :<| as) = trace "Seq is NOT Empty" $ do
            result <- lift $ step a as
            case result of
                Continue nextQ -> worker nextQ
                Output oneResult nextQ -> do
                    modify (oneResult :)
                    if not (isStuck oneResult)
                        then worker nextQ
                        else do
                            stuck <- gets (filter isStuck)
                            if maxCounterExamples <= Limit (fromIntegral (length stuck))
                                then
                                    pure $
                                        GotStuck (Seq.length nextQ) (mapMaybe extractState stuck)
                                else worker nextQ
                Abort _lastState queue -> do
                    pure $ Aborted $ toList queue

I traced this function calls and figured out that the given claim makes this function two recursive calls: the first one through non-empty sequence branch and the second one through empty sequence branch. During this calls ProofDepth doesn't change. So we get the warning.

Changing ProofDepth happens in trackProofDepth function:

...
let proofDepth' = (if didRewrite proofState' then succ else id) proofDepth
...
  where
    didRewrite proofState' =
        isApply prim
            && ClaimState.isRewritable proofState
            && isRewritten proofState'

    isApply Prim.ApplyClaims = True
    isApply Prim.ApplyAxioms = True
    isApply _ = False

    isRewritten (ClaimState.Rewritten _) = True
    isRewritten ClaimState.Proven = True
    isRewritten _ = False

So if we want to understand the warning origin we need to go deeper and understand why didRewrite returns False

[alexd1971]

I removed all claim simplifications during initialization:

@@ -947,7 +948,7 @@ initializeAndSimplify ::
     VerifiedModule StepperAttributes ->
     Simplifier Initialized
 initializeAndSimplify verifiedModule =
-    initialize (lift . simplifyRuleLhs >=> Logic.scatter) verifiedModule
+    initialize (lift . (\rule -> return $ MultiAnd.make [rule]) >=> Logic.scatter) verifiedModule

 -- | Collect various rules and simplifiers in preparation to execute.
 initialize ::
@@ -995,12 +996,12 @@ initializeProver definitionModule specModule maybeTrustedModule = do
     let Initialized{rewriteRules} = initialized
         changedSpecClaims :: [MaybeChanged SomeClaim]
         changedSpecClaims = expandClaim tools <$> extractClaims specModule
-        simplifyToList :: SomeClaim -> Simplifier [SomeClaim]
-        simplifyToList rule = do
-            simplified <- simplifyRuleLhs rule
-            let result = toList simplified
-            when (null result) $ warnTrivialClaimRemoved rule
-            return result
+        -- simplifyToList :: SomeClaim -> Simplifier [SomeClaim]
+        -- simplifyToList rule = do
+        --     simplified <- simplifyRuleLhs rule
+        --     let result = toList simplified
+        --     when (null result) $ warnTrivialClaimRemoved rule
+        --     return result

         trustedClaims :: [SomeClaim]
         trustedClaims = maybe [] extractClaims maybeTrustedModule
@@ -1012,22 +1013,23 @@ initializeProver definitionModule specModule maybeTrustedModule = do
     -- This assertion should come before simplifying the claims,
     -- since simplification should remove all trivial claims.
     assertSomeClaims specClaims
-    simplifiedSpecClaims <- mapM simplifyToList specClaims
-    claims <- traverse simplifySomeClaim (concat simplifiedSpecClaims)
+    -- simplifiedSpecClaims <- mapM simplifyToList specClaims
+    -- claims <- traverse simplifySomeClaim (concat simplifiedSpecClaims)
     let axioms = coerce <$> rewriteRules
         alreadyProven = trustedClaims
+        claims = specClaims
     pure InitializedProver{axioms, claims, alreadyProven}

After that the following claims was obtained:

Claim in yaml-report:

\implies{SortGeneratedTopCell{}}(
    \and{SortGeneratedTopCell{}}(
    \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}(Var''Unds''DotVar0:SortGeneratedCounterCell{}, Lbl''-LT-''generatedCounter''-GT-''{}(
  Var''Unds''DotVar2:SortInt{}) ), Lbl''-LT-''generatedTop''-GT-''{}(Lbl''-LT-''k''-GT-''{}(
  kseq{}(inj{SortBool{}, SortKItem{}}(
  Lbl''Unds''func-and''UndsUnds''AND-SYNTAX''Unds''Bool''Unds''Bool''Unds''Bool{}(
  Lbl''Unds''func-and''UndsUnds''AND-SYNTAX''Unds''Bool''Unds''Bool''Unds''Bool{}(
  \dv{SortBool{}}("true"), \dv{SortBool{}}("false")),
  Lbl''Unds''func-and''UndsUnds''AND-SYNTAX''Unds''Bool''Unds''Bool''Unds''Bool{}(
  \dv{SortBool{}}("true"), \dv{SortBool{}}("true") ) ) ),
  Var''Unds''DotVar1:SortK{} ) ), Lbl''-LT-''generatedCounter''-GT-''{}(
  Var''Unds''DotVar2:SortInt{} ) ) ), weakAlwaysFinally{SortGeneratedTopCell{}}(
  Lbl''-LT-''generatedTop''-GT-''{}(
  Lbl''-LT-''k''-GT-''{}(kseq{}(inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("false") ), Var''Unds''DotVar1:SortK{} ) ),
  Lbl''-LT-''generatedCounter''-GT-''{}(
  Var''Unds''DotVar2:SortInt{}
  ) ) ) )

And claim from frontend:

\implies{SortGeneratedTopCell{}} (
      \and{SortGeneratedTopCell{}} (
      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(
      kseq{}(inj{SortBool{}, SortKItem{}}(Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(\dv{SortBool{}}("true"),\dv{SortBool{}}("false")),Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(\dv{SortBool{}}("true"),\dv{SortBool{}}("true")))),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
      \and{SortGeneratedTopCell{}} (
      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("false")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))

So they differ in several places.

After that expandSingleConstructors was additionally removed:

@@ -1012,22 +1013,23 @@ initializeProver definitionModule specModule maybeTrustedModule = do
     -- This assertion should come before simplifying the claims,
     -- since simplification should remove all trivial claims.
     assertSomeClaims specClaims
-    simplifiedSpecClaims <- mapM simplifyToList specClaims
-    claims <- traverse simplifySomeClaim (concat simplifiedSpecClaims)
+    -- simplifiedSpecClaims <- mapM simplifyToList specClaims
+    -- claims <- traverse simplifySomeClaim (concat simplifiedSpecClaims)
     let axioms = coerce <$> rewriteRules
         alreadyProven = trustedClaims
+        claims = specClaims
     pure InitializedProver{axioms, claims, alreadyProven}
   where
     expandClaim ::
         SmtMetadataTools attributes ->
         SomeClaim ->
         MaybeChanged SomeClaim
-    expandClaim tools claim =
-        if claim /= expanded
-            then Changed expanded
-            else Unchanged claim
-      where
-        expanded = expandSingleConstructors tools claim
+    expandClaim tools claim = Unchanged claim
+      --   if claim /= expanded
+      --       then Changed expanded
+      --       else Unchanged claim
+      -- where
+      --   expanded = expandSingleConstructors tools claim

And we obtained:

Claim from yaml-output:

\implies{SortGeneratedTopCell{}}(
  \and{SortGeneratedTopCell{}}(
  \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(
  Lbl'-LT-'k'-GT-'{}( kseq{}( inj{SortBool{},
  SortKItem{}}(Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(
  Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(
  \dv{SortBool{}}("true"), \dv{SortBool{}}("false")
  ), Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(
  \dv{SortBool{}}("true"), \dv{SortBool{}}("true")
  ))), Var'Unds'DotVar1:SortK{})), Var'Unds'DotVar0:SortGeneratedCounterCell{}
  )), weakAlwaysFinally{SortGeneratedTopCell{}}(
  Lbl'-LT-'generatedTop'-GT-'{}(
  Lbl'-LT-'k'-GT-'{}( kseq{}( inj{SortBool{}, SortKItem{}}( \dv{SortBool{}}("false")
  ), Var'Unds'DotVar1:SortK{} ) ), Var'Unds'DotVar0:SortGeneratedCounterCell{}
  ) ) )

Claim from frontend:

\implies{SortGeneratedTopCell{}} (
  \and{SortGeneratedTopCell{}} (
  \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(
  Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBool{},
  SortKItem{}}(Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(
  Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(
  \dv{SortBool{}}("true"),\dv{SortBool{}}("false")
  ),Lbl'Unds'func-and'UndsUnds'AND-SYNTAX'Unds'Bool'Unds'Bool'Unds'Bool{}(
  \dv{SortBool{}}("true"),\dv{SortBool{}}("true")
  ))), Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}
  )), weakAlwaysFinally{SortGeneratedTopCell{}} (
      \and{SortGeneratedTopCell{}} (
      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("false")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))

At the beginning both are the same and difference appears only here:

weakAlwaysFinally{SortGeneratedTopCell{}}(
  Lbl'-LT-'generatedTop'-GT-'{}(
  Lbl'-LT-'k'-GT-'{}( kseq{}( inj{SortBool{}, SortKItem{}}( \dv{SortBool{}}("false")
  ), Var'Unds'DotVar1:SortK{} ) ), Var'Unds'DotVar0:SortGeneratedCounterCell{}
  ) ) )

---

weakAlwaysFinally{SortGeneratedTopCell{}} (
      \and{SortGeneratedTopCell{}} (
      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortBool{}, SortKItem{}}(\dv{SortBool{}}("false")),Var'Unds'DotVar1:SortK{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}))))

[ana-pantilie]

The proper solution for this issue would be to keep the original claims around when proving. I'm not sure how to make this change as non-invasive as possible, so I'd suggest we do the following first and see if it's acceptable.

For https://github.com/runtimeverification/haskell-backend/issues/3377, we need to pass the original list of claims (before calling those functions above which process them) to the proving functions as well, until we get to https://github.com/runtimeverification/haskell-backend/blob/0d66d723909dbeb90000771ac6a6b99491b917c9/kore/src/Kore/Reachability/Claim.hs#L329. That's where, on the ApplyClaims branch we will be applying the original list of claims.

For this issue, at https://github.com/runtimeverification/haskell-backend/blob/0d66d723909dbeb90000771ac6a6b99491b917c9/kore/src/Kore/Log/DebugRewriteTrace.hs#L86 we should be keeping a source location instead of that TermLike (https://github.com/runtimeverification/haskell-backend/blob/master/kore/src/Kore/Attribute/SourceLocation.hs).