The new rotl functions can exhibit undefined behavior when amt = 0.

[weaversa]

The new rotl functions can exhibit UB when amt = 0.

$ make prove
clang xxhash32-ref.c -o xxhash32-ref.bc -c -emit-llvm -Wno-long-long -O1 -std=c90
clang xxhash64-ref.c -o xxhash64-ref.bc -c -emit-llvm -Wno-long-long -O1 -std=c90
saw saw/xxhash32.saw
[18:12:55.128] Loading file "xxhash-clean/saw/xxhash32.saw"
[18:12:55.130] Loading file "xxhash-clean/saw/llvm.saw"
[18:12:55.426] Verifying XXH_rotl32 ...
[18:12:55.426] Simulating XXH_rotl32 ...
[18:12:55.430] Checking proof obligations XXH_rotl32 ...
[18:12:55.439] Subgoal failed: XXH_rotl32 safety assertion:
LLVM Poison value created
The second operand of `lshr` was equal to or greater than the number of
bits in the first operand
in XXH_rotl32 at internal
Details:
Undefined behavior encountered: 
LLVM Poison value created
The second operand of `lshr` was equal to or greater than the number of
bits in the first operand
Reference: 
The LLVM language reference, version8
‘lshr’ Instruction (Semantics)
Document URL: https://llvm.org/docs/LangRef.html

[18:12:55.439] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 30}
[18:12:55.439] ----------Counterexample----------
[18:12:55.439]   amt: 0
[18:12:55.440] ----------------------------------
[18:12:55.440] Stack trace:
"llvm_verify" (xxhash-clean/saw/xxhash32.saw:41:22-41:33):
"crucible_llvm_verify" (xxhash-clean/saw/llvm.saw:37:3-37:23):
Proof failed.
make: *** [prove] Error 2

Originally posted by @weaversa in #2 (comment)
I don't know if you saw the comment on the closed issue so I opened a new one.