suspicious Coq code for ACSL lemma in Frama-C 21

Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information.

Before submitting the issue, please confirm (by adding a X in the [ ]):

• the issue has not yet been reported on Gitlab;
• the issue has not yet been reported on our BTS;
• you installed Frama-C as prescribed in the instructions.

Contextual information

• Frama-C installation mode: opam
• Frama-C version: 21.0 (Scandium)
• Plug-in used: WP
• OS name: macOS
• OS version: 10.15.5

Please add specific information deemed relevant with regard to this issue.

Steps to reproduce the issue

The following ACSL lemma in file a.c

/*@
  lemma C_Division_Two:
    \forall integer a; 0 <= a  ==>  0 <= a/2 <= a;
 */

is verified by Alt-Ergo when calling it with

frama-c-gui -wp -wp-prover alt-ergo -wp-prover native:coq a.c

However, in Frama-C 21, the coq representation of the lemma looks wrong to me since it reads

Goal
  forall (i : Z),
  ((0 <= i)%Z) ->
  (((((Cdiv i 2)) <= i)%Z) /\ (((-1) <= i)%Z)).

The -1 does not seem to be right.

In Frama-C 20, on the other hand, the coq representation looks like this

Goal
  forall (i : Z),
  let x := ((Cdiv i 2))%Z in
  ((0 <= i)%Z) ->
  (((x <= i)%Z) /\ ((0 <= x)%Z)).

Am I missing something here?