• David Hauzar's avatar
    Adding information about the line that corresponds to the VC check · 68b3134d
    David Hauzar authored
    to the counter-example model.
    
    This line must be marked with the label "model_vc".
    If VC line is postcondition, it can be marked with the label
    "model_func" or "model_func:func_name". Terms corresponding to
    old values of arguments will be marked with @old, term corresponding
    to the function result will be marked with @result or
    func_name@result if func_name was given.
    
    Pretty printing of model element names in counter-example.
    Possibility to print differently model elements corresponding to
    function result, old values of function arguments and other model
    elements.
    68b3134d
model_parser.mli 6.63 KB