From bfbd39c2a7d8e4c12385ce965d08e4fac921f025 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 6 Nov 2020 06:15:54 -0800
Subject: [PATCH] [sledge] Interpret conversions between float types as
 identity

Summary:
Since floats of any width are interpreted the same (as exact rationals
where possible and uninterpreted constants otherwise), this does not
introduce additional infidelity.

Reviewed By: da319

Differential Revision: D24746225

fbshipit-source-id: bc8e7bdb9
---
 sledge/src/llair_to_Fol.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index 5ede842a4..d45e7ed2b 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -87,6 +87,7 @@ and term : Llair.Exp.t -> T.t =
         | _ -> uap1 (Unsigned bits) a
       else uap1 (Unsigned bits) a
   | Ap1 (Convert {src= Pointer _}, Pointer _, e) -> term e
+  | Ap1 (Convert {src= Float _}, Float _, e) -> term e
   | Ap1 (Convert {src}, dst, e) ->
       let s =
         Format.asprintf "convert_%a_of_%a" Llair.Typ.pp dst Llair.Typ.pp src