• Sylvain Dailler's avatar
    Removes model_trace added at parsing · 786526f4
    Sylvain Dailler authored
    Removes debug flag: debug_auto_model.
    Some changes in counterexamples triggered by:
    - (non counterexamples) transformations which have a specific case for
       model_trace but not for the new detection: this is intended as
       simplifications that would be done are often simplifications we want
       for counterexamples,
    - Some locations are missing in variables introduced by SP/WP which should
      explain the rest.
    
    This also disables projections for record in intro_projection_counterexmp.
    
    Correct subst_filter to be consistent with new counterexample modification
    786526f4
Name
Last commit
Last update
..
glob.ml Loading commit data...
glob.mli Loading commit data...
lexer.mli Loading commit data...
lexer.mll Loading commit data...
parser.mly Loading commit data...
ptree.ml Loading commit data...
typing.ml Loading commit data...
typing.mli Loading commit data...