• David Hauzar's avatar
    Traceability for record field names in counterexamples. · b25b6a72
    David Hauzar authored
    In wp, eval_match is used to replace record fields with simple variables
    of the same type. Originally, all labels from the variable that field
    was accessed were copied to new variables representing fields of this
    variable. Therefore also "model_trace:var_name" label was copied and thus
    the field had name "var_name" in the counterexample.
    
    This commit solves this problem by appending names of the fields to
    "model_trace:*" label of new variables representing record fields.
    b25b6a72
eval_match.ml 7.17 KB