Configuration not fully rewriten

Two rules that look like this: rule lhs => rhs1 requires cond and rule lhs => rhs2 requires not cond, do not fully rewrite a configuration.

Versions:

$ kompile --version
K version:    v5.5.132-0-g96ce008122-dirty
Build date:   Tue Mar 07 16:08:12 EET 2023

$ kore-exec --version
Kore version 0.60.0.0
Git:
  revision:     559424aa4841449a0e83d7c555264d68b03cf475
  branch:       HEAD
  last commit:  Fri Mar 3 05:02:43 2023 -0700

To reproduce:
a.k:

module A
  imports BOOL
  imports INT
  imports MAP

  syntax Intw ::= wrap(Int)

  syntax KItem ::= b(Int, Int, Map)

  rule b(X, Y, M) => 0
      requires wrap(X modInt 2) in_keys(M) andBool wrap(Y) in_keys(M)
  rule b(X, Y, M) => 1
      requires notBool (wrap(X modInt 2) in_keys(M) andBool wrap(Y) in_keys(M))
endmodule

proof.k:

module PROOF
  imports A

  claim b(_, _, _) => ?_:Int
endmodule

Command line:

kompile a.k --backend haskell && kprove proof.k

Output:

kore-exec: [566480] Warning (WarnStuckClaimState):
    The configuration's term doesn't unify with the destination's term and the configuration cannot be rewritten further. Location: /mnt/data/runtime-verification/elrond-wasm/.build/bug-report/proof.k:4:9-4:29
Context:
    (InfoReachability) while checking the implication
  #Not ( {
      true
    #Equals
      wrap ( _Gen0 modInt 2 ) in_keys ( _Gen2 )
    }
  #And
    {
      true
    #Equals
      wrap ( _Gen1 ) in_keys ( _Gen2 )
    } )
#And
  #Not ( {
    false
  #Equals
    wrap ( _Gen0 modInt 2 ) in_keys ( _Gen2 ) andBool ( wrap ( _Gen1 ) in_keys ( _Gen2 ) )
  } )
#And
  <k>
    b ( _Gen0 , _Gen1 , _Gen2 ) ~> _DotVar1 ~> .
  </k>

Start by running the reproduction with a.k and proof.k using kompile --backend haskell followed by kprove, and inspect the WarnStuckClaimState output. Trace how the two conditional rules are applied to the b(_, _, _) claim. Done means the configuration fully rewrites and the claim no longer gets stuck.