From f59dda2f665e0e99320cde3e52799eeaa404e9ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 31 Jan 2020 10:39:56 +0100
Subject: [PATCH] [Eva] Fixes eval_term: removes NaN from the ival used for
mathematical reals.
---
src/plugins/value/legacy/eval_terms.ml | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 5b24b23e4f4..c9607a9d98d 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -296,6 +296,12 @@ let c_logic_var lvi =
(Base.of_c_logic_var lvi), ty
| _ -> unsupported_lvar lvi
+let top_float =
+ let neg_infinity = Fval.F.of_float neg_infinity
+ and pos_infinity = Fval.F.of_float infinity in
+ let fval = Fval.inject ~nan:false Fval.Real neg_infinity pos_infinity in
+ Ival.inject_float fval
+
let bind_logic_vars env lvs =
let bind_one (state, logic_vars) lv =
let bind_logic_var ival =
@@ -303,7 +309,7 @@ let bind_logic_vars env lvs =
in
match Logic_utils.unroll_type lv.lv_type with
| Linteger -> bind_logic_var Ival.top
- | Lreal -> bind_logic_var Ival.top_float
+ | Lreal -> bind_logic_var top_float
| _ ->
try
let b, cty = c_logic_var lv in
--
GitLab