When parsing an integer from the same string twice, GNATprove doesn't accept that the same integer should be produced twice. How should I rectify this?

Main file:

with String_Problem;

procedure Eq_Test is
begin
   String_Problem.String_Equal("4456");
end Eq_Test;

String_Problem.ads:

package String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   with
       Ghost;
end String_Problem;

String_Problem.adb:

package body String_Problem
with Spark_Mode
is
   procedure String_Equal
     (A : String)
   is
      X1 : Integer;
      X2 : Integer;
   begin
      X1 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      X2 := Integer'Value (A);
      pragma Annotate
        (Gnatprove, False_Positive, "precondition might fail", "we only call on valid integer strings");
      pragma Assert (X1 = X2);
   end String_Equal;
end String_Problem;

GNATProve output:

alr gnatprove
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...

string_problem.adb:16:22: medium: assertion might fail
   16 |      pragma Assert (X1 = X2);
      |                     ^~~~~~~
Summary logged in [path]/gnatprove/gnatprove.out