diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 72aaae64939db4a472ba53182119724d895b22c0..a48ee527aeb89e68f42cbc68c9c9c2127b0687e0 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