MurmurHash/SMHasher author here. While I don't doubt this passes BigCrush etc, I do find it very surprising that it does.
The state update function is effectively "a = rotate(a, constant) + b; b = rotate(b, constant) + constant;" and the output derivation is "output = (a + b) * constant".
That update function is _barely_ nonlinear, and the output derivation is linear. The output would probably be slightly better as "(a ^ b) * constant".
The slow_loop thing to guarantee 2^128 period is probably not needed - anyone with an application that cares about a period that high is probably going to choose a more robust generator (a few rounds of hardware-accelerated AES in counter mode is your best bet there)
The use of the Z3 prover is neat and I should read up on that more.
The state update function is effectively "a = rotate(a, constant) + b; b = rotate(b, constant) + constant;" and the output derivation is "output = (a + b) * constant".
That update function is _barely_ nonlinear, and the output derivation is linear. The output would probably be slightly better as "(a ^ b) * constant".
The slow_loop thing to guarantee 2^128 period is probably not needed - anyone with an application that cares about a period that high is probably going to choose a more robust generator (a few rounds of hardware-accelerated AES in counter mode is your best bet there)
The use of the Z3 prover is neat and I should read up on that more.