--- integer rules, exact int32 wraparound, for every constant listed ---
ok  (x*3)*5 -> x*15                                            proved for every input   [0.0s]
ok  (x+3)+5 -> x+8                                             proved for every input   [0.0s]
ok  (x+3)*5 -> x*5+15                                          proved for every input   [0.0s]
ok  (x*-2)*7 -> x*-14                                          proved for every input   [0.0s]
ok  (x+-2)+7 -> x+5                                            proved for every input   [0.0s]
ok  (x+-2)*7 -> x*7+-14                                        proved for every input   [0.0s]
ok  (x*4)*4 -> x*16                                            proved for every input   [0.0s]
ok  (x+4)+4 -> x+8                                             proved for every input   [0.0s]
ok  (x+4)*4 -> x*4+16                                          proved for every input   [0.0s]
ok  (x*1)*-1 -> x*-1                                           proved for every input   [0.0s]
ok  (x+1)+-1 -> x+0                                            proved for every input   [0.0s]
ok  (x+1)*-1 -> x*-1+-1                                        proved for every input   [0.0s]
ok  x%2 == x-(2*(x//2))                                        proved for every input   [0.0s]
ok  x%3 == x-(3*(x//3))                                        proved for every input   [1.1s]
ok  x%4 == x-(4*(x//4))                                        proved for every input   [0.0s]
ok  x%7 == x-(7*(x//7))                                        proved for every input   [2.8s]
ok  x%16 == x-(16*(x//16))                                     proved for every input   [0.0s]
ok  (x//2)//3 -> x//6   (c1,c2 > 0)                            proved for every input   [2.4s]
ok  (x//4)//4 -> x//16   (c1,c2 > 0)                           proved for every input   [0.0s]
ok  (x//3)//5 -> x//15   (c1,c2 > 0)                           proved for every input   [22.0s]
ok  (x//8)//2 -> x//16   (c1,c2 > 0)                           proved for every input   [0.0s]
ok  x//1 and x%1                                               proved for every input   [0.0s]
ok  x//-1 and x%-1                                             proved for every input   [0.0s]
ok  x//0 == 0 and x%0 == x (the total contract)                proved for every input   [0.0s]
ok  INT_MIN // -1 == INT_MIN (wraps)                           proved for every input   [0.0s]
--- 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.3s]
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]
--- range rule: x in [lo, lo+c-1] with lo//c == hi//c means x%c == x - c*(lo//c) ---
ok  x in [8,11] -> x%4 == x-8                                  proved for every input   [0.0s]
ok  x in [8,11] -> x//4 == 2                                   proved for every input   [0.0s]
ok  x in [12,17] -> x%6 == x-12                                proved for every input   [0.0s]
ok  x in [12,17] -> x//6 == 2                                  proved for every input   [0.0s]
ok  x in [-10,-6] -> x%5 == x--10                              proved for every input   [0.0s]
ok  x in [-10,-6] -> x//5 == -2                                proved for every input   [0.0s]
--- float32 rules, with z3's IEEE floating point theory ---
ok  x*1.0 -> x                                                 proved for every input   [0.0s]
ok  x+(-0.0) -> x                                              proved for every input   [0.0s]
ok  x+0.0 -> x (the unsafe one)                                COUNTEREXAMPLE f=-0.0, fp.to_ieee_bv=[else -> fp.to_ieee_bv(Var(0))]   [0.0s]
ok  x*0.0 -> 0.0 (the unsafe one)                              COUNTEREXAMPLE f=-oo, fp.to_ieee_bv=[NaN -> 2147483583, else -> fp.to_ieee_bv(Var(0))]   [0.0s]
ok  (x+y)+z -> x+(y+z) (the unsafe one)                        COUNTEREXAMPLE h=-1.50781333446502685546875*(2**70), g=-1.62500095367431640625*(2**66), f=1.00000059604644775390625*(2**91), fp.to_ieee_bv=[else -> fp.to_ieee_bv(Var(0))]   [0.6s]
ok  x*(1/x) -> 1.0 (the unsafe one)                            COUNTEREXAMPLE f=NaN, fp.to_ieee_bv=[NaN -> 4286611488, else -> fp.to_ieee_bv(Var(0))]   [1.0s]
ok  -(-x) -> x                                                 proved for every input   [0.0s]
ok  x*-1.0 -> -x                                               proved for every input   [0.0s]
ok  -(x*y) -> x*(-y)                                           proved for every input   [0.1s]
ok  max(x,y) -> max(y,x) on floats (the unsafe one)            COUNTEREXAMPLE g=+0.0, f=-0.0, fp.to_ieee_bv=[else -> fp.to_ieee_bv(Var(0))]   [0.0s]
ok  x+(-x) -> 0.0 on floats (the unsafe one)                   COUNTEREXAMPLE f=+oo, fp.to_ieee_bv=[NaN -> 2145152384, else -> fp.to_ieee_bv(Var(0))]   [0.0s]
ok  max(x,x) -> x on floats                                    proved for every input   [0.0s]
ok  x+y == y+x                                                 proved for every input   [0.0s]
ok  x*y == y*x                                                 proved for every input   [0.0s]

59 of 59 claims came out as expected
