diff --git a/src/transform/intro_vc_vars_counterexmp.ml b/src/transform/intro_vc_vars_counterexmp.ml index e94d5cce0bd7e9b49b23a58ab30b94c6506fa843..8ebf80549827026ee510fc986dc55c86e01b02c4 100644 --- a/src/transform/intro_vc_vars_counterexmp.ml +++ b/src/transform/intro_vc_vars_counterexmp.ml @@ -84,8 +84,7 @@ let model_trace_for_postcondition ~labels = (* Modifies the model_trace label of a term in the postcondition: - if term corresponds to the initial value of a function parameter, model_trace label will have postfix @old - - if term corresponds to the return value of a function, add - model_trace label in a form function_name@result + Returns labels with model_trace label modified if there exist model_trace label in labels, labels otherwise. *)