From 60e28f582b37d4080686992ea114857f75cfe6c2 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 31 Oct 2020 09:23:53 +0100
Subject: seems to work better

---
 backend/CSE3analysis.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 7316c9a9..5eb92a82 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -282,12 +282,14 @@ Section OPERATIONS.
 
   Definition oper2 (dst : reg) (op: sym_op)(args : list reg)
            (rel : RELATION.t) : RELATION.t :=
-    let rel' := kill_reg dst rel in
     match eq_find {| eq_lhs := dst;
                      eq_op  := op;
                      eq_args:= args |} with
-    | Some id => PSet.add id rel'
-    | None => rel'
+    | Some id =>
+      if PSet.contains rel id
+      then rel
+      else PSet.add id (kill_reg dst rel)
+    | None => kill_reg dst rel
     end.
 
   Definition oper1 (dst : reg) (op: sym_op) (args : list reg)
-- 
cgit