Remove precondition check for SOME transitive closure eliminators.

WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic

MIT License

5 stars 0 forks source link

Closed nancyday closed 4 months ago

nancyday commented 4 months ago

Input file: expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/CaseStudies/PTCRISync/ptcris_v0_6_0_draft_BASE7.smttc

After running MaxUnboundedScopesCompiler, it gives:

Exception in thread “main” fortress.util.Errors$Internal$PreconditionError: Precondition violated: sort in closure must be bounded