Mentions légales du service

Skip to content
  • Sylvain Dailler's avatar
    fix #160 · dfab5cb0
    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