Unsimplified expression in side condition

Note that this spec is not supposed to pass, it was drastically changed form the original in order to reduce the size of the files below.

To reproduce:

Versions

kompile:

K version:    v5.5.40-0-g98574f12a2-dirty
Build date:   Wed Dec 07 16:21:49 EET 2022

backend:

Kore version 0.60.0.0
Git:
  revision:     bdfc0fa4b0e381b3d02551ab0d4b4f89cedf814b
  branch:       HEAD
  last commit:  Wed Nov 30 06:11:08 2022 -0700

Files

a.k

module A
    imports BOOL
    imports INT
    imports K-EQUAL

    configuration
      <esdt>
        <is-running> #no:Running </is-running>
        
        <shards>
          <shard multiplicity="*" type="Map">
            <shard-id> 0:Int </shard-id>
            <steps> .K </steps>
            <current-tx> 0 </current-tx>
          </shard>
        </shards>
      </esdt>

    syntax Running ::= "#no"
                     | Int

    syntax TxStep ::= #failure( Int )
                    | "#finalizeTransaction"

     rule <shard> 
            <steps> (#failure(_Err) => .) ~> #finalizeTransaction </steps>
            <current-tx> _Tx </current-tx>
            ...
          </shard>

    // Check if the execution cells (<current-tx/> and <steps/>) in all shards are empty
    syntax Bool ::= #allEmpty(ShardsCell)   [function, total]
    rule #allEmpty(S) => #allEmptyHelper(S, true)
    syntax Bool ::= #allEmptyHelper(ShardsCell, Bool)   [function, total]
    rule #allEmptyHelper(<shards> .Bag </shards>, true) => true
    rule #allEmptyHelper(_, false) => false
    rule #allEmptyHelper(<shards>
                    (<shard> 
                      <steps> Ss </steps>
                      <current-tx> Tx </current-tx>
                      _          
                    </shard> => .Bag
                    )
                    ...
                  </shards>
                  , B => B andBool (Ss =/=K .K orBool Tx =/=K 0)
                  ) [simplification]
    rule #allEmptyHelper(S, (_ andBool _) #as Cond) => #allEmptyHelper(S, true) andBool Cond [simplification]
    rule #allEmptyHelper(S, (_ orBool _) #as Cond) => #allEmptyHelper(S, true) andBool Cond [simplification]

endmodule

spec.k

requires "a.k"

module SPEC
    imports A

    claim
      <is-running> ShrId </is-running>
      <shards>
        <shard>
          <shard-id> ShrId </shard-id>

        // Execution
          <current-tx> 1 </current-tx>
          <steps> . => #finalizeTransaction </steps>
        
          ...
        </shard>
        OtherShards
      </shards>
      requires #allEmpty(<shards> OtherShards </shards>)

endmodule

Running

Command line:

kompile a.k --backend haskell && kprove --debug spec.k --haskell-backend-command 'kore-repl --version --repl-script ../kast.kscript'

repl:

step
select 1
konfig

Results

Note that the displayed config contains this:

#And
  {
    true
  #Equals
    notBool ( #failure ( _Err ) ~> #finalizeTransaction ~> . ) ==K . orBool notBool _Tx ==Int 0
  }

which should be simplified to Top.

Start by running the supplied kompile, kprove, and kore-repl commands with a.k and spec.k, then inspect the displayed configuration after step and select 1. Trace why the side condition remains as an #And expression instead of simplifying to Top; done means the reproduced configuration shows the simplified result.