search

EasyCrypt / easycrypt

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

[smt]: proper selection of SMT variant #586

Closed strub closed 4 months ago

strub commented 4 months ago

Why3 can define several variants (e.g. counterexamples, noBV).

Currently, EasyCrypt select the first variant that comes in the prover list. From now on, the default variant (= empty name) is selected by default. It is also possible to provide the desired in the prover name (syntax = "prover[variant]", e.g. "Z3[noBV]").

This is compatible with the version selection (e.g. "Z3[noBV]@4.8")

strub commented 4 months ago

Note that this might explain partially why some smt calls where unstable. It seems that this breaks a few calls here and there, but for the best.