[Why3 Error] Type mismatch between ieee float.Float32.t and real
- Frama-C installation mode: Opam
- Frama-C version: 22.0 (Titanium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: Ubuntun 20.04.1 LTS
Please add specific information deemed relevant with regard to this issue.
Steps to reproduce the issue
Downloads the test_frama-c.c file. This file contains 3 functions (
test_3) which are functionally identical but differ by the added asserts.
Run the command :
frama-c-gui -wp -wp-model real -wp-prover alt-ergo,z3-ce,cvc4-strings-ce -rte test_frama-c.c
All the goals should be proved.
Only the function
test_2 is verified, but the functions
test_3 are not verified and I get from Why3 the error:
[Why3 Error] Type mismatch between ieee_float.Float32.t and real
I also tested with the
-wp-prover native:alt-ergo and
-wp-model with the same result.