WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic
MIT License
5 stars 0 forks source link

Properly handle shadowing in MaxAlphaRenaming #148

Closed ryandancy closed 2 months ago

ryandancy commented 2 months ago

MaxAlphaRenaming completely failed to handle variable shadowing before (oops!). Now it's handled properly.

Once this was fixed I was still getting an error in the OPFI test that was failing because the solution found had x = 0, which seemed to be a valid solution even though the intention was for the only allowable solution to be x = -1. So I modified the test to explicitly disallow x = 0.