Bitwuzla: Fix performance issues in FloatingPointFormulaManagerTest

[daniel-raffler]

Hello, this MR aims to fix the performance issues described in #371. The problem was not about the conversion operation itself, but about the large number of ProverEnvironments that would be created, one for each test input. We solve this by reusing the same ProverEnvironment for all inputs of the test. This also improves the performance of Z3 for those same tests.

In addition to that the MR includes a number of minor fixes:

• Bitwuzla does not support float-to-bitvector conversions and we are using a work-around that introduces new side-conditions for the casts. We now make sure that side-conditions are only pushed onto the stack when needed. The old version would simply include everything in the query, even for variables that don't occur in the assertions, which can cause significant overhead
• We fixed the names that are used for the variables in these side-conditions to make sure that there are no clashes
• FunctionDeclarationKind gets a new Symbol FP_REM which was missing
• We also added support for BV_SHR and BV_ROL, BV_ROLI, BV_ROR, BV_RORI to the Bitwuzla FormulaCreator

[daniel-raffler]

Thanks for the review! I've opened a new issue about the rotations (https://github.com/sosy-lab/java-smt/issues/397). Once this has been resolved the workaround can be removed here. I've also added some more documentations about getVariableCasts() and merged the calculation into a single function.