EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

Get rid of unbounded smt calls outside examples #420

Closed oskgo closed 1 year ago

oskgo commented 1 year ago

I used the following regex on all the .ec and .eca files outside the examples folder: (^|[^o])smt[^\(]*(\.|;|\(.*@.*\)).

I left most the smt(... @Theory ...) invocations be for now.

I updated some of the invocations using old syntax that matched my regex as well.