Failed to prove unsigned addition with overflow

Just installed Frama-C 28.1 (Nickel) and it seems that Frama-C can't prove even unsigned addition out of the box for me.

Given the file file.c:

#include <limits.h>

/*@ 
  @ assigns \nothing;
  @ 
  @ behavior wont_overflow:
  @   assumes x + y <= UINT_MAX;
  @   ensures \result == (x + y) % (UINT_MAX + 1); // TODO: it's general ensure
  @   ensures \result >= x;
  @
  @ behavior will_overflow:
  @   assumes x + y > UINT_MAX;
  @   ensures \result == (x + y) % (UINT_MAX + 1); // TODO: it's general ensure
  @   ensures \result < x;
  @
  @ complete behaviors wont_overflow, will_overflow;
  @ disjoint behaviors wont_overflow, will_overflow;
  @*/
unsigned uAdd(unsigned x, unsigned y) {
    return x + y;
}

Running

frama-c -wp -wp-rte -rte file.c

outputs

[kernel] Parsing file.c (with preprocessing)
[rte:annot] annotating function uAdd
[wp] 7 goals scheduled
[wp] [Timeout] typed_uAdd_will_overflow_ensures_2 (Qed 0.70ms) (Alt-Ergo)
[wp] [Timeout] typed_uAdd_will_overflow_ensures (Qed 0.72ms) (Alt-Ergo)
[wp] Proved goals:    7 / 9
  Terminating:       1
  Unreachable:       1
  Qed:               3
  Alt-Ergo 2.5.3:    2 (9ms-12ms)
  Timeout:           2

showing that both ensure statements of will_overflow behavior were timeouted.

What's wrong? Perhaps the CLI flags?

The current integer theory does not have the right formulation to allow the proof to be tackled automatically by SMT solvers. Another version is under development, but in the mean time, one can use the Overflow tactic to finish the proof from the GUI:

Result:

Tactical Overflow: (proved)
Sub Goals:
 - In-Range : proved
 - Lower : proved
 - Upper : proved

Once the script has been executed, it can be saved in the session and reused when replaying the proof using the prover script (-wp-prover alt-ergo,script).