Commit b093a9ac authored by Clément Fumex's avatar Clément Fumex

fix merge

parent 69cecb03
......@@ -185,9 +185,9 @@ let timeout_handler () =
try
for _i = Queue.length prover_tasks_in_progress
to 3 * !max_number_of_running_provers do
let (c,id,pr,timelimit,callback) = Queue.pop scheduled_proof_attempts in
let (c,id,pr,limit,callback) = Queue.pop scheduled_proof_attempts in
try
build_prover_call c id pr timelimit callback
build_prover_call c id pr limit callback
with e when not (Debug.test_flag Debug.stack_trace) ->
Format.eprintf
"@[Exception raised in Controller_itp.build_prover_call:@ %a@.@]"
......
......@@ -827,14 +827,15 @@ and merge_trans env old_s new_s new_goal_id old_tr_id =
let new_subtasks = List.map (fun id -> id,new_s)
new_tr.transf_subtasks in
let associated,detached =
AssoGoals.associate ~use_shapes:true old_subtasks new_subtasks
AssoGoals.associate ~use_shapes:false old_subtasks new_subtasks
in
List.iter (function
| ((new_goal_id,_), Some ((old_goal_id,_), obsolete)) ->
Debug.dprintf debug "[merge_theory] pairing paired one goal, yeah !@.";
merge_goal env new_s old_s obsolete (get_proofNode old_s old_goal_id) new_goal_id
| (_, None) ->
Debug.dprintf debug "[merge_theory] pairing found missed sub goal :( @.";
| ((id,s), None) ->
Debug.dprintf debug "[merge_theory] pairing found missed sub goal :( : %s @."
(get_proofNode s id).proofn_name.Ident.id_string;
found_missed_goals_in_theory := true)
associated;
(* save the detached goals *)
......@@ -883,7 +884,7 @@ let merge_theory env old_s old_th s th : unit =
(* attach the session to the subtasks to be able to instantiate Pairing *)
let detached_goals = Hstr.fold (fun _key g tl -> (g,old_s) :: tl) old_goals_table [] in
let associated,detached =
AssoGoals.associate ~use_shapes:true detached_goals !new_goals
AssoGoals.associate ~use_shapes:false detached_goals !new_goals
in
List.iter (function
| ((new_goal_id,_), Some ((old_goal_id,_), obsolete)) ->
......
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