Skip to content

Commit

Permalink
[cvc5 mappings] Fix argument type
Browse files Browse the repository at this point in the history
  • Loading branch information
joaomhmpereira authored and filipeom committed Jun 17, 2024
1 parent 9be702f commit a71c8f6
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions lib/cvc5_mappings.default.ml
Original file line number Diff line number Diff line change
Expand Up @@ -280,8 +280,7 @@ module Fresh_cvc5 () = struct
match Float.is_nan f with
| true -> Term.mk_fp_nan tm es eb
| _ ->
let b = int_of_float f in
let bt = Term.mk_bv tm (es + eb) b in
let bt = Term.mk_bv tm (es + eb) (Int64.of_float f) in
Term.mk_fp tm es eb bt

let neg t = Term.mk_term tm Kind.Floatingpoint_neg [| t |]
Expand Down

0 comments on commit a71c8f6

Please sign in to comment.