search

boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
506 stars 111 forks source link

Only async call to M #905

Closed NamrathaG closed 2 months ago

NamrathaG commented 2 months ago

Calls to procedures that are later refined using the ISR rule must be async calls. This is needed to apply the ISR rule.

NamrathaG commented 2 months ago

Looks good to me. Let's merge!