alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

to_finit: fix issue #526

Browse source 
* spot/twaalgos/remprop.cc: Use bdd_restrict instead of bdd_exists.
* tests/core/ltlf.test: Add test case.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2023-02-07 14:40:20 +01:00
parent 058975c167
commit 6fd0eebad4
3 changed files with 57 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -22,6 +22,10 @@ New in spot 2.11.3.dev (not yet released)
done in Spot so far) may require the output to use transition-based
acceptance. (Issue #525.)
- to_finite(), introduce in 2.11, had a bug that could break the
completeness of automata and trigger an exception from the HOA
printer. (Issue #526.)
New in spot 2.11.3 (2022-12-09)
Bug fixes: