From 92cca153569e44cd11ba3d1b68c2708c0cc46899 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@lilo.org>
Date: Wed, 28 Jul 2021 17:00:02 +0200
Subject: ci fix?

---
 scheduling/BTLtoRTLproof.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'scheduling/BTLtoRTLproof.v')

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 324f1d14..4ef55928 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -232,6 +232,8 @@ Proof.
     inv MIB. exists pc'; split; auto; constructor.
     apply plus_one. inv LOAD.
     eapply exec_Iload; eauto.
+    2: destruct (eval_addressing _ _ _ _) eqn:EVAL;
+    [ eapply exec_Iload_notrap2 | eapply exec_Iload_notrap1]; eauto.
     all: erewrite <- eval_addressing_preserved; eauto;
          intros; rewrite symbols_preserved; trivial.
   - (* exec_store *)
-- 
cgit