Condition from branch not taken kept in the main configuration

This seems to decrease the performance significantly on certain proofs.

To reproduce:

tmp.k

module TMP
  imports MAP
  imports INT

  syntax KItem ::= a(Map) | "b" | "c" | d(Map)
  rule b => c
  rule d(M:Map) => a(M)

  syntax Int ::= count(Map) [function, functional]
  rule count(.Map) => 0
  rule count(K |-> _ M) => 1 +Int count(M) ensures notBool K in_keys(M)
  [simplification]
endmodule

tmp-proof.k

module TMP-PROOF
  imports TMP

  claim a(_ |-> _ M:Map) => b requires count(M) >Int 5
  [trusted]

  claim a(_ |-> _ M:Map) => b requires count(M) >Int 3
  [trusted]

  claim a(M:Map) => b requires count(M) >Int 0
  [trusted]

  claim d(M:Map) => c requires count(M) >Int 0 andBool count(M) <Int 3
endmodule

command line:

kompile tmp.k --backend haskell && \
    kprove tmp-proof.k --haskell-backend-command "kore-repl --smt-timeout 1000 --repl-script kast.kscript"

repl:

stepf 5
select 3
konfig

Note that at step 1 -> 2 the REPL tried to apply 3 claims. For two of them, the SMT solver said that the condition is unsat, so the backend didn't try to take those branches. However, when applying the third, the Haskell backend kept the negated conditions from those branches (although they should always be true):

  #Not ( #Exists _0 . #Exists _1 . #Exists M0 . {
      M
    #Equals
      M0
      _0 |-> _1
    }
  #And
    {
      false
    #Equals
      _0 in_keys ( M0 )
    }
  #And
    {
      true
    #Equals
      count ( M0 ) >Int 3
    } )
#And
  #Not ( #Exists _0 . #Exists _1 . #Exists M0 . {
      M
    #Equals
      M0
      _0 |-> _1
    }
  #And
    {
      false
    #Equals
      _0 in_keys ( M0 )
    }
  #And
    {
      true
    #Equals
      count ( M0 ) >Int 5
    } )
#And
  <k>
    c ~> _DotVar1 ~> .
  </k>
#And
  {
    true
  #Equals
    count ( M ) <Int 3
  }
#And
  {
    true
  #Equals
    count ( M ) >Int 0
  }

Reproduce the issue with tmp.k and tmp-proof.k using the stated kompile and kprove commands, then run the REPL sequence stepf 5, select 3, and konfig. Inspect how the Haskell backend carries conditions from claims whose SMT checks were unsatisfiable; done means the displayed configuration no longer retains negated conditions from those unchosen branches.