From 319e6d2f0b75911094d5cd182be9355a08777fc5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 2 Apr 2020 16:53:58 +0200
Subject: [PATCH] [logic-interp] avoid creating non-supported long-double ops
---
src/kernel_services/analysis/logic_interp.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index 99fd4b2c8a7..ca8044ead8d 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -200,7 +200,7 @@ let rec logic_type_to_typ = function
| Ctype typ -> typ
| Linteger -> TInt(ILongLong,[]) (*TODO: to have an unlimited integer type
in the logic interpretation*)
- | Lreal -> TFloat(FLongDouble,[]) (* TODO: handle reals, not floats... *)
+ | Lreal -> TFloat(FDouble,[]) (* TODO: handle reals, not floats... *)
| Ltype({lt_name = name},[]) when name = Utf8_logic.boolean ->
TInt(ILongLong,[])
| Ltype({lt_name = "set"},[t]) -> logic_type_to_typ t
--
GitLab