Fix bvlshr name and add a test.

[vakaras]

No description provided.

[marcoeilers]

LGTM! We might want to add either a single link to the SMTLIB description of these functions or, if we're adding functions that aren't in that description for some reason (I didn't see bvashr either), maybe we should just add a comment per function that describes what it does.

[vakaras]

LGTM! We might want to add either a single link to the SMTLIB description of these functions or, if we're adding functions that aren't in that description for some reason (I didn't see bvashr either), maybe we should just add a comment per function that describes what it does.

@Aurel300 Is there a specific document in which you found bvashr? I found the functions I added here.

[Aurel300]

@Aurel300 Is there a specific document in which you found bvashr? I found the functions I added here.

The function itself is mentioned in the guide. In the text above there is a dead link, but it is preserved on the web archive—maybe this is what the source was? There is also the source code. The documentation for Z3 is pretty bad…

[vakaras]

The SMT and Z3 documentations are really amazing. I assume that Z3 supports a union of the mentioned functions…

[vakaras]

@ArquintL Will the IDE CI automatically pick up this change, or do I need to do anything special?

[ArquintL]

@ArquintL Will the IDE CI automatically pick up this change, or do I need to do anything special?

ViperServer repo should identify this commit tomorrow morning and in turn trigger a new nightly build of the ViperTools in the Viper-IDE repo

[vakaras]

@ArquintL Will the IDE CI automatically pick up this change, or do I need to do anything special?

ViperServer repo should identify this commit tomorrow morning and in turn trigger a new nightly build of the ViperTools in the Viper-IDE repo

Sounds great!