Printing floating points

[Ola Fosheim Grøstad]

On Friday, 29 January 2021 at 21:11:02 UTC, sarn wrote:
> Have you seen KLEE?  It applies a solver like Z3 to normal code 
> with assert() statements, as long as it can be compiled to LLVM 
> bitcode and run with KLEE-compatible standard libraries.

I've only read about KLEE, which looks interesting. Using LLVMIR  
is one approach one can use for analysis when the input/output is 
tiny. You can (after unrolling) convert the IR  to  64 logical 
propositions. One big logical (boolean) formula for each bit in 
the output.

In this specific application you could try to prove that output 
bit 1 only depends on input bit 1, output bit 2 only depends on 
input bit 2 and so on.

(After applying the inverse function, so that the function 
returns the same value as the input.)