-
David Hauzar authored
triggering VC. - Transformation intro_vc_vars_counterexamp introduces new constant with model labels for every variable in the term that trigger VC and axiom that this constant is equal to the variable, finds the position of the term that trigger VC, and saves this position in meta (for smtv2 printer). - Transformation prepare_for_counterexmp additionally performs the transformation intro_vc_vars_counterexamp - smtv2 printer no longer collects the location of the term that triggers VC and does not collect variables in this term in a special way. Note that this functionality was not yet completely removed from the printer. It will be done so after the transformation intro_vc_vars_counterexmp will be tested. The rationale: Variables that should be displayed in counterexample are marked by model labels ("model", "model_projected", "model_trace:*"). Variables inside the term that triggers VC should be displayed in counterexample for that VC. However, many VCs (tasks) can be generated for a signle *.mlw file and only variables in the term that trigger the VC (task) that is currently proven should be displayed. That means that the process of selecting variables inside the term that triggers VC for counterexample must be done while processing the task. It is done by transformation intro_vc_vars_counterexmp. This means that smtv2 printer no longer has to find the position of the term that triggers VC and no longer has to collect variables in this term in a special way.
0b53e050