[Why3 Error] Type mismatch between ieee float.Float32.t and real
Contextual information
- 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_1, test2
andtest_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
Expected behaviour
All the goals should be proved.
Actual behaviour
Only the function test_2
is verified, but the functions test_1
and 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.