WP goals: cannot prove some properties related to integer division/modulo
File: div-mod.i
L1 and L2 cannot be proved with Colibri2. I have used the SMT2 file exported for CVC5 for reduction.
L3 and L4 cannot be proved with Colibri2, but I suspect the Colibri2 Why3 driver. In particular, Colibri2 do prove the goal generated for CVC5.