Unexpected behavior when using shift and multiplication

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: 22.0 (Titanium)
• Plug-in used: WP
• OS name: Ubuntu
• OS version: Ubuntun 20.04.1 LTS

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

Steps to reproduce the issue

1. Get the following C file (issue_shift.c):

#include <limits.h>

/*@
  requires 0 <= a <= 16;
  assigns \nothing;
*/
int test(int a){
  int tmp = (a * a) >> 2;
  //@ assert assert_tmp: 0 <= tmp <= 64;

  //@ assert assert_mult: 0 <= tmp * tmp <= INT_MAX;
  return a * a;
}

2. Run the command : frama-c-gui -wp -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte issue_shift.c

Expected behaviour

All the goals should be proved.

Actual behaviour

The assertion assert_mult is not verified. Indeed, when a variable is the result of a shift, the multiplication of this variable cannot be bound.

However, if we test with:

int tmp = 32;
//@ assert 0 <= tmp * tmp <= INT_MAX

The assertion is proved.

I tried to define the following lemma to help the provers but without success.

/*@ lemma bound_mult: 
    \forall int a;
     0 <= a <= 64
     ==> 0 <= a * a <= INT_MAX;
*/