From 731d22f1b917a3e55deb82505fc5f981b4a37bcc Mon Sep 17 00:00:00 2001
From: Pierre Goutagny <pierre.goutagny@ens-lyon.fr>
Date: Fri, 4 Jun 2021 13:45:59 +0200
Subject: Fix check_instr Icond target conditions

---
 backend/RTLTunneling.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'backend/RTLTunneling.v')

diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v
index 4885002f..e6901a9f 100644
--- a/backend/RTLTunneling.v
+++ b/backend/RTLTunneling.v
@@ -63,8 +63,8 @@ Definition check_instr (td: UF) (pc: node) (i: instruction): res unit :=
       | Icond _ _ ifso ifnot _ =>
           let (tso,dso) := get td ifso in
           let (tnot,dnot) := get td ifnot in
-          if peq tpc ifso then
-            if peq tpc ifnot then
+          if peq tpc tso then
+            if peq tpc tnot then
               if zlt dso dpc then
                 if zlt dnot dpc then OK tt
                 else Error (msg "bad distance on else branch")
-- 
cgit