From 3ceff391e0be39cd7a3d5d861fb1f32653579bab Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 15 Oct 2020 11:50:56 +0200
Subject: some more tuning of CSE3

---
 backend/CSE3analysisproof.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index 0ddaa527..66b199cc 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -821,7 +821,11 @@ Section SOUNDNESS.
       subst.
       rewrite <- (forward_move_sound rel rs m r) by auto.
       apply move_sound; auto.
-    - destruct rhs_find as [src |] eqn:RHS_FIND.
+    - destruct (is_trivial_sym_op sop).
+      {
+        apply kill_reg_sound; auto.
+      }
+      destruct rhs_find as [src |] eqn:RHS_FIND.
       + destruct (Compopts.optim_CSE3_glb tt).
         * apply sem_rel_glb; split.
           ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND.
-- 
cgit