Wrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC4
On the following example:
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
The following command fails:
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover exit status: exited with status 1
Prover output:
(error "expecting an integer subterm")
...
Apparently, in_range
is transformed into abs 0.0
which requires an int. Note that on Why3 1.2.1, the file contains a definition abs1
for real numbers, but the generated goal uses abs
(leading to the same error). If in_range
is used in a lemma or an axiom, the same bug happens.