diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 0aed56e5f..377fcda33 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -425,6 +425,8 @@ let smt_fpa_builtins = end | Id { ns = Term ; name = Simple "ae.float16" } -> term_app env s (smt_round 11 24) + | Id { ns = Term ; name = Simple "bv2int" } -> + term_app1 env s DE.Term.Bitv.to_nat | Id { ns = Term ; name = Simple "ae.float32" } -> term_app env s (smt_round 24 149) | Id { ns = Term ; name = Simple "ae.float64" } ->