diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index 30ccf50da..7bc002b90 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -106,6 +106,8 @@ namespace spot formula* unabbreviate_logic(const formula* f) { + if (f->is_sugar_free_boolean()) + return f->clone(); unabbreviate_logic_visitor v; const_cast(f)->accept(v); return v.result(); diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 294a0da1a..1392b41b1 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -289,6 +289,8 @@ namespace spot formula* negative_normal_form(const formula* f, bool negated) { + if (!negated && f->is_in_nenoform()) + return f->clone(); negative_normal_form_visitor v(negated); const_cast(f)->accept(v); return v.result(); diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index b6567e282..498bae629 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -98,6 +98,8 @@ namespace spot formula* simplify_f_g(const formula* f) { + if (f->is_boolean()) + return f->clone(); simplify_f_g_visitor v; const_cast(f)->accept(v); return v.result(); diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 21c65d59a..7bbcd6cc2 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -70,6 +70,8 @@ namespace spot formula* unabbreviate_ltl(const formula* f) { + if (f->is_sugar_free_boolean() && f->is_sugar_free_ltl()) + return f->clone(); unabbreviate_ltl_visitor v; const_cast(f)->accept(v); return v.result();