[Move-prover][Bitwise] Add support for vector::insert & bug fix for handling the let expression in the spec

move-language / move

Apache License 2.0

2.26k stars 688 forks source link

[Move-prover][Bitwise] Add support for vector::insert & bug fix for handling the let expression in the spec #878

Closed rahxephon89 closed 1 year ago

rahxephon89 commented 1 year ago

Motivation

This PR 1) adds supports for handling vector::insert function for bitwise operations; 2) fix a bug when handling let expression in the spec for bv types.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

bitwise_features.move is modified to test the change.