Adding a mini CSE pass in the expansion oracle

1 files changed, 3 insertions, 3 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index f0def29b..20d9e1da 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -641,11 +641,11 @@ Opaque Int.eq.
       apply exec_straight_one. simpl; reflexivity. auto. 
       split; intros; Simpl. }
   (* Expanded instructions from RTL *)
-  7,8,15,16:
+  7,14:
     econstructor; split; try apply exec_straight_one; simpl; eauto;
-    split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl;
+    split; intros; Simpl; simpl;
     try rewrite Int.add_commut; try rewrite Int64.add_commut;
-    destruct (rs (preg_of m0)); try discriminate; eauto.
+    auto.
   1-12:
     destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0;
     econstructor; split; try apply exec_straight_one; simpl; eauto;