From d7b3d05e5722103070b59108444c6cf8d9d80322 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 9 Jun 2020 20:23:42 +0200
Subject: [PATCH] minato: use bdd_ite()

* spot/misc/minato.cc: Use bdd_ite() to exercise one of the function
rewritten in the next patch, and also because that is supposedly
faster.
---
 spot/misc/minato.cc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spot/misc/minato.cc b/spot/misc/minato.cc
index 596341d1c..331eeaa1e 100644
--- a/spot/misc/minato.cc
+++ b/spot/misc/minato.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2009, 2013-2015, 2020 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -166,7 +166,7 @@ namespace spot
             continue;
 
           case local_vars::FourthStep:
-            ret_ |= (l.g0 - l.v1) | (l.g1 & l.v1);
+            ret_ |= bdd_ite(l.v1, l.g1, l.g0);
             todo_.pop();
             continue;
           }