Skip to content

Conversation

@kroening
Copy link
Collaborator

The numbering that Spot uses for the atoms in the given formula need not match ours; hence, this adds parsing for the AP: header in Spot's HOA output.

These tests reproduce a problem where our numbering for atomic propositions
differs from Spot's.
The numbering that Spot uses for the atoms in the given formula need not
match ours; hence, this adds parsing for the "AP:" header in Spot's HOA
output.
@kroening kroening marked this pull request as ready for review October 31, 2025 19:09
@tautschnig tautschnig merged commit 941b266 into main Nov 1, 2025
11 checks passed
@tautschnig tautschnig deleted the hoa-AP-fix branch November 1, 2025 17:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants