--- the divisible-terms split: (a*k*c + b)//c -> a*k + b//c ---
ok  (a*4+b)//4 -> a*1+b//4  when a*4 and the sum fit           proved for every input   [0.2s]
ok  (a*4+b)%4 -> b%4  when a*4 and the sum fit                 proved for every input   [0.0s]
ok  (a*4+b)//4 -> a*1+b//4  WITHOUT the guard                  COUNTEREXAMPLE a=1073741824, b=-2147483648   [0.0s]
ok  (a*24+b)//8 -> a*3+b//8  when a*24 and the sum fit         proved for every input   [0.1s]
ok  (a*24+b)%8 -> b%8  when a*24 and the sum fit               proved for every input   [0.0s]
ok  (a*24+b)//8 -> a*3+b//8  WITHOUT the guard                 COUNTEREXAMPLE a=457266860, b=1929388032   [0.0s]
--- the same split for divisors that are not powers of two, over mathematical integers (z3 bit vectors time out on division by 3) ---
ok  (a*6+b)//3 -> a*2+b//3  (integers, guarded)                proved for every input   [0.0s]
ok  (a*6+b)%3 -> b%3  (integers, guarded)                      proved for every input   [0.0s]
ok  (a*15+b)//5 -> a*3+b//5  (integers, guarded)               proved for every input   [0.0s]
ok  (a*15+b)%5 -> b%5  (integers, guarded)                     proved for every input   [0.0s]
ok  (a*35+b)//7 -> a*5+b//7  (integers, guarded)               proved for every input   [0.0s]
ok  (a*35+b)%7 -> b%7  (integers, guarded)                     proved for every input   [0.0s]
ok  (a*6+b)//6 -> a*1+b//6  (integers, guarded)                proved for every input   [0.0s]
ok  (a*6+b)%6 -> b%6  (integers, guarded)                      proved for every input   [0.0s]
