Failure to prune branch with a boolean function involving `==K`

[goodlyrottenapple]

The backend fails to simplify a boolean function involving ==K when the function occurs inside a requires clause.

This is a minimal example which reproduces the bug:

verification.k

module VERIFICATION
    imports BOOL
    imports K-EQUAL

    syntax Bar ::= "AA" | "BB" | Bar2

    syntax Bar2 ::= "CC" Bar3

    syntax Bar3 ::= "DD" | "EE"

    syntax KItem ::= Bar

    syntax Bool ::= #isAorB ( Bar ) [function, total]

    rule #isAorB(OP) => OP ==K AA orBool OP ==K BB

    syntax KItem ::= runLemma ( Bool )
                   | runLemma2 ( Bool )
                   | doneLemma( Bool )
 // --------------------------------------
    rule <k> runLemma( T ) => doneLemma( T ) ... </k>

    rule <k> ( runLemma2( T ) => doneLemma ( false ) ) ... </k> requires notBool T
    rule <k> ( runLemma2( T ) => doneLemma ( true ) ) ... </k> requires T

endmodule

spec.k

requires "verification.k"

module SPEC

imports VERIFICATION
imports BOOL

claim <k> runLemma ( #isAorB ( CC _ ) ) => doneLemma ( false ) ... </k>

claim <k> runLemma2 ( #isAorB ( CC _ ) ) => doneLemma ( false ) ... </k>

endmodule

Note that runLemma simply forces the evaluation of #isAorB ( CC _ ) into false, however runLemma2 makes two branches, one for evaluating to doneLemma ( false ) and another to doneLemma ( true ) based on a requires notBool #isAorB ( CC _ ) and requires #isAorB ( CC _ ) respectively.

The backend fails to prune the second branch, as it fails to rewrite true #Equals #isAorB ( CC _ ) to #Bottom even tho it was able to rewrite #isAorB ( CC _ ) into false on the other branch (this can be checked by disabling rule <k> ( runLemma2( T ) => doneLemma ( true ) ) ... </k> requires T ):

➜ kompile verification.k --backend haskell --no-haskell-binary
➜ kprove spec.k                                               
kore-exec: [213254] Warning (WarnStuckClaimState):
    The configuration's term doesn't unify with the destination's term and the configuration cannot be rewritten further. Location: /Users/sam/git/evm-semantics/spec.k:10:7-10:73
Context:
    (InfoReachability) while checking the implication
  <k>
    doneLemma ( true ) ~> _DotVar1 ~> .
  </k>
#And
  {
    true
  #Equals
    ( CC _Gen0 ~> . ) ==K ( AA ~> . ) orBool ( CC _Gen0 ~> . ) ==K ( BB ~> . )
  }
[Error] Prover: backend terminated because the configuration cannot be
rewritten further. See output for more details.