Validity of simple existential pattern over map not proven

Bug report

Z3 version 4.8.7 - 64 bit

K version:    5.1.226
Build date:   Tue Oct 12 02:23:45 CEST 2021

kompile --backend haskell assign.k && kprove --def-module VERIFICATION spec.k

assign.k

module ASSIGN-SYNTAX
  imports INT-SYNTAX
  imports ID-SYNTAX

  syntax Stmt ::= Id "=" Int
endmodule

module ASSIGN
  imports ASSIGN-SYNTAX
  imports INT
  imports MAP

  configuration
    <T>
      <k>
        $PGM:Stmt
      </k>
      <env>
        .Map
      </env>
    </T>

  rule <k> X:Id = V:Int => . ... </k>
       <env> M => M [X <- V] </env>
endmodule

spec.k

requires "assign.k"

module SPEC-SYNTAX
  imports ASSIGN-SYNTAX

  syntax Id ::= "$x" [token]
endmodule

module VERIFICATION
  imports SPEC-SYNTAX
  imports ASSIGN
endmodule

module SPEC
  imports VERIFICATION

  claim <k> $x = A:Int => . ... </k>
        <env> M => M [ $x <- ?B:Int ] </env>
    ensures A <=Int ?B
endmodule

Expected output

#Top

Actual output

  #Not ( #Exists ?B . {
      M [ $x <- ?B:Int ]
    #Equals
      M [ $x <- A:Int ]
    }
  #And
    {
      true
    #Equals
      A <=Int ?B
    } )
#And
  <T>
    <k>
      _DotVar2
    </k>
    <env>
      M [ $x <- A:Int ]
    </env>
  </T>

Note: The claim is proven if the property is strengthened to equality, i.e. with ensures A ==Int ?B.

Reproduce the behavior with assign.k and spec.k using kompile and kprove as shown, comparing the expected #Top result with the actual existential constraint. Start by tracing how the Haskell backend handles existential patterns over map updates; done means the original inequality claim is proven as expected without weakening it to equality.