Infinite loop when branching, on the remainder branch

Versions:

$ kompile --version
K version:    v6.0.57-0-ga91e8fd25a-dirty
Build date:   Jo aug 31 13:43:29 EEST 2023

$ kore-repl --version
Kore version 0.60.0.0
Git:
  revision:     3cfcc04ac3d0db7dd37487ed901700ed0f6f6450
  branch:       HEAD
  last commit:  Tue Aug 1 15:57:31 2023 +0100

Minimized example:
a.k:

module A-SYNTAX
  imports BOOL
  syntax A ::= "a" | "b" | split(Bool)
endmodule

module A
  import A-SYNTAX
  import BOOL
  import INT

  syntax Bool ::= f(Int, Int)  [function, total, no-evaluators]
  syntax Int ::= g(Int, Int)  [function, total, no-evaluators]
  syntax Int ::= h(Int, Int)  [function, total, no-evaluators]

  rule VAL1 +Int VAL2 <Int MAX => true requires VAL1 <Int MAX andBool VAL2 <Int MAX andBool f(VAL1, VAL2) [simplification]

  rule split(B:Bool) => .K requires B
  rule split(B:Bool) => .K requires notBool B

  rule h(Val, Max) => h(Val +Int Max, Max) requires Val <Int 0 andBool 0 <Int Max
endmodule

spec.k:

module SPEC
  imports A
  claim split(M <=Int Z) => .K
      requires X ==Int Y *Int M +Int Z
          andBool g(X, M) ==Int g(Z, M)
          andBool Y ==Int h(X -Int Z, M)
          andBool 0 <Int M
endmodule

Command line:

$ kompile a.k --backend haskell && kprove spec.k

As far as I can tell, executing the split produces a remainder with M <=Int Z and #Not(M <=Int Z) and the backend tries to prune the remainder branch.

However, when doing that, it tries first to simplify h(X -Int Z, M). When simplifying, the Haskell backend may or may not check that the side condition is satisfiable (it is, anyway), but then it checks that the rule does not leave a remainder. When doing that, it checks that (not <rule-condition>) and <side-condition> is not satisfiable, which is not, since the side condition is #bottom. This makes the backend apply the simplification rule. After that, the backend attempts to simplify the result, which means that it attempts to apply the same simplification rule, which succeeds, which causes an infinite loop.

Reproduce the issue with kompile a.k --backend haskell && kprove spec.k, using the minimized a.k and spec.k examples. Start by tracing Haskell-backend remainder pruning while simplifying h(X -Int Z, M). Done means the proof no longer loops and the remainder branch terminates correctly.