-
Sylvain Dailler authored
This fixes a problem in the wp generation and eval match where it was possible to create new variables with same labels (including model_trace) which does not have the same type. This results in bad typing for counterexamples. In particular, when only one region of a type is mutable we can project directly during wp (now we do the same but with the corresponding model_trace).
dfab5cb0