• 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
bench Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
stdlib Loading commit data...
tests Loading commit data...
why3-coq.opam Loading commit data...
why3-ide.opam Loading commit data...
why3.opam Loading commit data...
.dockerignore Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
.ocp-indent Loading commit data...
AUTHORS Loading commit data...
CHANGES.md Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL.md Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README.md Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...