Commit ab23b00a by Sylvain Dailler

fixes #33

Check that both the name and the arguments are the same when loading a transformation.
parent 35418b73
Pipeline #10485 passed with stage
in 3 minutes 13 seconds
module T
goal G: False
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../33_reload_trans.mlw">
<theory name="T" sum="f6c01df1ed5265da509017649b093f5e">
<goal name="G">
<transf name="assert" arg1="(1 = 1)">
<goal name="G.0">
</goal>
<goal name="G.1">
</goal>
</transf>
<transf name="assert" arg1="(0 = 0)">
<goal name="G.0">
</goal>
<goal name="G.1">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -1440,7 +1440,10 @@ let apply_trans_to_goal ~allow_no_effect s env name args id =
let add_registered_transformation s env old_tr goal_id =
let goal = get_proofNode s goal_id in
try
let _tr = List.find (fun transID -> (get_transfNode s transID).transf_name = old_tr.transf_name)
let _tr = List.find (fun transID -> (get_transfNode s transID).transf_name = old_tr.transf_name &&
List.fold_left2 (fun b new_arg old_arg -> new_arg = old_arg && b) true
(get_transfNode s transID).transf_args
old_tr.transf_args)
goal.proofn_transformations in
(* NOTE: should not happen *)
Debug.dprintf debug "[add_registered_transformation] transformation already present@.";
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment