Mentions légales du service

Skip to content

smtv2-model-parser: improve conversion from sort to ty

Guillaume Cluzel requested to merge smtv2_model_parser-handle-more-types into master

On top of !862 (merged) to avoid conflicts as much as possible. It will be easier to read once !862 (merged) is merged.

This MR improves the conversion from SMTV2 sorts to Why3 by keeping a table that stores an injection from the sorts to the Why3 types and that is filled when the smtv2 task is created.

The name of prover builtin are also kept to be able to find the original name in the Why3 code.

Merge request reports