• Sylvain Dailler's avatar
    Keeping keep_on_simp labels during wp generation. · 64b1fda4
    Sylvain Dailler authored
    We changed t_map_simp, track_values and the eval_match transformation
    in order to prevent them from removing terms whose head has label
     keep_on_simp. Note that simplification inside those terms is
    still possible.
    
    * src/core/term.ml
    (t_map_simp): Adding the case when f has label keep_on_simp.
    
    * src/transform/eval_match.ml
    (eval_match): Adding keep_on_simp as a stop label.
    
    * src/whyml/mlw_wp.ml
    (track_values): Stopping on keep_on_simp label.
    64b1fda4
mlw_wp.ml 82.6 KB