Printing floating points

[sarn]

On Friday, 29 January 2021 at 18:48:42 UTC, Ola Fosheim Grøstad 
wrote:
> And you would also need to annotate the D code with Hoare logic 
> and generate verification conditions. Although there are tools 
> that can help with that. But you would still need expertise to 
> make good use of it. It is not a push-button topic.
>
> The only other alternative would be bit blasting, as I 
> mentioned, which may or may not work out. Probably not if the 
> code is too convoluted, but it might. Depends on the solver and 
> structure of the input.

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.

The original KLEE doesn't support floating point, but there's a 
fork that does (which I've never used).

https://theartofmachinery.com/2019/05/28/d_and_klee.html
(There are some things I need to fix/update in that post.)