search

mit-plv / fiat

Mostly Automated Synthesis of Correct-by-Construction Programs
http://plv.csail.mit.edu/fiat/
Other
147 stars 31 forks source link

More reasonable implementation of add_resolve_to_db. #109

Closed ppedrot closed 5 months ago

ppedrot commented 5 months ago

We stop relying on Hints.hint_constr and only add terms that look like a global reference. All callers are respecting this precondition as they go through a variant of abstract.

(If I didn't screw up this should be backwards compatible even with 8.19.)