feature wish: possibility to disable automatic conversion between bool and prop
Why3 silently applies conversions between bool and prop when user input is wrongly typed:
- if
t
has type bool and a prop is expected, replace byt=True
- if
t
is prop and a bool is expected, replace byif t then True else False
Of course these simplifies the life of the user, by they may have impact, e.g. on inference of invariants. In particular the rule 2 above tends to produce significantly complex terms, whereas the user would have written something simpler if he/she knew that there was a type clash.
I wonder if the default could be to apply only rule 1, having an option (via command-line, meta, etc.) to allow rule 2 or conversely to even forbid rule 1