search

marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Better tuple axiomatization #173

Closed marcoeilers closed 7 months ago

marcoeilers commented 9 months ago

Also moving some stuff from type domain factory to resource files

This change is Reviewable

PascalDevenoge commented 8 months ago

@marcoeilers Might be good to get this merged. I'm not sure what's causing the test failure, is there a quick way to fix this?

marcoeilers commented 8 months ago

Something is unsound about one of the new axioms (or about some type signature), Carbon can sometimes prove false. I've stared at this a bunch last week but haven't found the issue yet. But that needs to be fixed before I can merge this.