From 4b5da92387c775d258503189cf6dc92f37a1b28e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 24 Apr 2019 21:08:08 +0200
Subject: [PATCH] [Eva] Fixes a crash on logic coercions from booleans to
integers.
---
src/plugins/value/legacy/eval_terms.ml | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 72aaae64939..a48ee527aeb 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -887,9 +887,7 @@ let rec eval_term ~alarm_mode env t =
nothing to do, AND coercion from an integer type to a floating-point
type, that require a conversion. *)
(match Logic_const.plain_or_set Extlib.id ltyp with
- | Linteger ->
- assert (Logic_typing.is_integral_type t.term_type);
- r
+ | Linteger when Logic_typing.is_integral_type t.term_type -> r
| Ctype typ when Cil.isIntegralOrPointerType typ -> r
| Lreal ->
if Logic_typing.is_integral_type t.term_type
--
GitLab