From 3614cf34a8bbae7ce3b13dd6436673b1e52baa36 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 30 Jul 2021 12:05:21 +0200 Subject: [PATCH] use bdd_have_common_assignment in more places * spot/twaalgos/gfguarantee.cc, spot/twaalgos/isdet.cc: Use it. --- spot/twaalgos/gfguarantee.cc | 2 +- spot/twaalgos/isdet.cc | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/spot/twaalgos/gfguarantee.cc b/spot/twaalgos/gfguarantee.cc index 94496ee6e..f0aa58274 100644 --- a/spot/twaalgos/gfguarantee.cc +++ b/spot/twaalgos/gfguarantee.cc @@ -260,7 +260,7 @@ namespace spot // history further. if (hlen > 0) for (auto& ei: aut->out(moved_init)) - if ((ei.cond & econd) != bddfalse + if (bdd_have_common_assignment(ei.cond, econd) && term[si.scc_of(ei.dst)]) goto failed; diff --git a/spot/twaalgos/isdet.cc b/spot/twaalgos/isdet.cc index b7b6df0be..864a9315c 100644 --- a/spot/twaalgos/isdet.cc +++ b/spot/twaalgos/isdet.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2018, 2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -132,7 +132,7 @@ namespace spot // Second pass to gather the relevant edges. if (!universal) for (auto& t: aut->out(src)) - if ((t.cond & extra) != bddfalse) + if (bdd_have_common_assignment(t.cond, extra)) (*highlight)[aut->get_graph().index_of_edge(t)] = color; } aut->prop_universal(universal);