From eb1121d703835e76babc15b057276d2852ade4ab Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 16:25:46 +0100
Subject: totally switch off conditions in cse3

---
 backend/CSE3proof.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'backend/CSE3proof.v')

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 50a32d56..ca43d0bd 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -983,6 +983,8 @@ Proof.
         unfold find_cond_in_fmap in FIND_COND.
         change (@PMap.get (option RELATION.t)) with (@Regmap.get RB.t) in FIND_COND.
         rewrite FIND_REL in FIND_COND.
+        destruct (Compopts.optim_CSE3_conditions tt).
+        2: discriminate.
         destruct (is_condition_present pc rel cond args).
         { rewrite COND_PRESENT_TRUE in H0 by trivial.
           congruence.
-- 
cgit