From 01357e6f60be0621beb72764eba6f7e540b4266a 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:24:44 +0100
Subject: [PATCH] [Eva] Fixes eval_terms: unroll logic types.
---
src/plugins/value/legacy/eval_terms.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 13867fb6971..5b24b23e4f4 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -301,7 +301,7 @@ let bind_logic_vars env lvs =
let bind_logic_var ival =
state, LogicVarEnv.add lv (Cvalue.V.inject_ival ival) logic_vars
in
- match lv.lv_type with
+ match Logic_utils.unroll_type lv.lv_type with
| Linteger -> bind_logic_var Ival.top
| Lreal -> bind_logic_var Ival.top_float
| _ ->
@@ -319,7 +319,7 @@ let bind_logic_vars env lvs =
let unbind_logic_vars env lvs =
let unbind_one (state, logic_vars) lv =
- match lv.lv_type with
+ match Logic_utils.unroll_type lv.lv_type with
| Linteger | Lreal -> state, LogicVarEnv.remove lv logic_vars
| _ ->
let b, _ = c_logic_var lv in
--
GitLab