From f442f4e500be376aa75591a87cf8152e1032e8d0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 2 Mar 2020 14:35:01 +0100
Subject: [PATCH] [Eva] Subdivision: do not forget to clear the valuation
cache.
When the subdivision on a sub-expression [s] is performed according to [s] and
not according to the complete expression [e], we then reevaluate [e] with the
result of the subdivision. However, the valuation should be cleared before.
Otherwise, the reevaluation uses the cache and not the reduced values computed
by the subdivision.
---
src/plugins/value/engine/subdivided_evaluation.ml | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 57806d98601..8a9e11f7da7 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -787,6 +787,9 @@ module Make
instead of [expr]. Use [~expr:subexpr], then evaluate [expr]
with the reduced valuation, then continue to subdivide. *)
subdivide ~expr:subexpr ~subexpr >>> fun valuation _ _ ->
+ let valuation =
+ Clear.clear_englobing_exprs valuation ~expr ~subexpr
+ in
Eva.evaluate context valuation expr >>>
subdivide_subexpr tail
in
--
GitLab