• 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
ident.mli 7.17 KB