search

move-language / move

Apache License 2.0
2.26k stars 689 forks source link

[prover] Added a Boogie model for vector::insert function #831

Closed awelc closed 1 year ago

awelc commented 1 year ago

Motivation

A Boogie model is missing for recently added vector::insert function and this PR is attempting to remedy it

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

Added a spec for a function using vector::insert to the functional tests.