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);