frem discrepancy between alive2 and llvm

[bongjunj]

llvm/llvm-project#128457

3.0 frem 2.0 should result in 1.0 in llvm while alive2 thinks it to be -1.0

The value produced is the floating-point remainder of the two operands. This is the same output as a libm ‘fmod’ function, but without any possibility of setting errno. The remainder has the same sign as the dividend. This instruction is assumed to execute in the default floating-point environment. This instruction can also take any number of fast-math flags, which are optimization hints to enable otherwise unsafe floating-point optimizations:
frem Semantics, LLVM Reference

[aqjune]

Can we encode z = frem ty x, y as something like x - y * floor(x / y) on the SMT side? This can again be approximation because x / y cannot be infinitely precise, but still will be a better approximation.