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") ...
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.