From e1d751823e1dbc5cb6cb2d05203efd7c5d3883f9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 8 Sep 2020 18:28:56 +0200
Subject: [PATCH] [eva] factor identical cases in pattern-matching
---
src/plugins/value/engine/transfer_logic.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 4ee6f16a624..a6efdf17d21 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -688,8 +688,7 @@ module Make
aux_interp ~reduce code_annot behav p
in
match code_annot.annot_content with
- | AAssert (behav, p) ->
- aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
+ | AAssert (behav, p)
| AInvariant (behav, true, p) ->
aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
| APragma _
--
GitLab