Postcondition on a procedure doesn't prove even though the same condition is asserted and true at the end of procedure

The code looks like this:

spec:

type Some_Record_Type is private;

procedure Deserialize_Record_Y(Record: in out Some_Record_Type)
with Post => (
    if Status_OK then (
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record'Old)
    )
);

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type;
function Record_Field_X_Count(Record: Some_Record_Type) return Natural;

body:

type Some_Record_Type is
   record
      X_Count: Natural;
      X      : X_Bounded_Array_Type;
      Y_Count: Natural;
      Y      : Y_Bounded_Array_Type;
      ...
   end record;

function Record_Field_X(Record: Some_Record_Type) return X_Unbounded_Array_Type
is (
   ...
   a bit of logic based on values of other fields of Record
   ...
)

function Record_Field_X_Count(Record: Some_Record_Type) return Natural
is (Record.X_Count);

procedure Deserialize_Record_Y(Record: in out Some_Record_Type) is
    Old_Record: Some_Record_Type := Record with Ghost;
begin
    ...
    -- updates the Y field of the Record.
    -- Note that we annot pass Record.Y and have to pass
    -- the whole Record because Record is a private type
    -- and Deserialize_Record_Y is in public spec
    ...
    pragma Assert_And_Cut (
        Status_OK
        and then
        ...
        other postconditions
        ...
        and then
        Record_Field_X_Count(Record) = Record_Field_X_Count(Record_Old)
        and then
        Record_Field_X(Record) = Record_Field_X(Record_Old)
    )
end Deserialize_Record_Y;

There are no proof errors in the body, the error is only on the spec:

postcondition might fail, cannot prove Record_Field_X(Record) = Record_Field_X(Record'Old)

'other postconditions' are identical between the spec and the Assert_And_Cut at the end of the procedure.

Note the the checks with simpler fields, like X_Count:

Record_Field_X_Count(Record) = Record_Field_X_Count(Record'Old)

do not cause gnatprove to complain.

There's quite a lot of work for the prover inside the procedure, so usually, when there's a problem proving the postcondition it helps to assert that condition at the end of the procedure to 'remind' the prover that this is important facts. Usually, this works, but in one case it doesn't for some reason.

What are my options here?

What might be possible causes of this?

Maybe I should just increase the RAM on the machine where I run the proover, so it won't lose the Record_Field_X(Record) = Record_Field_X(Record_Old) fact between the end of the procedure and its postcondition? (I'm currently doing this on a machine with 32GB ram which is used exclusively to run gnatprove, with --memlimit=32000 --prover=cvc4,altergo --steps=0)

Maybe there are some techniques I don't know?

Maybe the only option I have is the manual proof?

I'm using the spark community 2019 version.

To summarize the comments, adding z3 to the provers with

--prover=cvc4,altergo,z3

helped to solve the problem.