Add support for Reals

[ThomasMayerl]

This PR adds support for Reals to Prusti with support for all of the operation on Reals that SMTLIB exposes. I also created tests for these operations.

[JonasAlaif]

Mostly tiny cosmetic/style changes

[Aurel300]

@ThomasMayerl It seems there's two new failures compared to the main branch?

• tests/verify/pass/equality/pure-post-5.rs - this now reaches unreachable.
• tests/verify/pass/floats/reals.rs - there are now some failing cases here, too. This might be related to the float changes from Update Viper toolchain to 2025-11-19 #125 though.

[ThomasMayerl]

• tests/verify/pass/floats/reals.rs - there are now some failing cases here, too. This might be related to the float changes from Update Viper toolchain to 2025-11-19 #125 though.

Regarding this, two testcases in this file are currently failing because the current z3 versions seem to not be able to reason about that somehow. I've opened a z3 issue but haven't gotten a reply yet. @JonasAlaif said it's still okay for Prusti as long as it generates correct code since it's nothing that we can fix

[ThomasMayerl]

• tests/verify/pass/equality/pure-post-5.rs - this now reaches unreachable.

As for this, I tried to analyze this a bit and here is what I found out: I had to switch the check for function calls whether the function call is pure or a builtin so that it checks the builtin first (because some of the Real's builtins are also pure). However, if you call find_impl_of_trait_method_call (to check if it's a builtin) for the pure-post-5.rs testcase, an unreachable is reached. As I did not change that function, I think that the issue does not come from this PR but rather already existed previously and that the error was just not triggered