• 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
..
jlamp0 Loading commit data...
oracles Loading commit data...
algebraic_type.mlw Loading commit data...
array_mono.mlw Loading commit data...
array_records.mlw Loading commit data...
arrays.mlw Loading commit data...
floats.mlw Loading commit data...
if_assign.mlw Loading commit data...
if_decision_branch.mlw Loading commit data...
int.mlw Loading commit data...
int32.mlw Loading commit data...
int_overflow.mlw Loading commit data...
jlamp0.mlw Loading commit data...
jlamp_array.mlw Loading commit data...
jlamp_projections.mlw Loading commit data...
list.mlw Loading commit data...
map.mlw Loading commit data...
polymorphism.mlw Loading commit data...
range_type.mlw Loading commit data...
real.mlw Loading commit data...
record_map.mlw Loading commit data...
record_one_field.mlw Loading commit data...
records.mlw Loading commit data...
records_inv.mlw Loading commit data...
records_label.mlw Loading commit data...
ref.mlw Loading commit data...
ref_mono.mlw Loading commit data...
result.mlw Loading commit data...
simple_array.mlw Loading commit data...