Skip to content
Snippets Groups Projects
Commit 72914e2f authored by David Bühler's avatar David Bühler
Browse files

[Eva] Partition: adds a comment to the function [combine] for ration stamps.

parent 145e07f9
No related branches found
No related tags found
No related merge requests found
...@@ -252,7 +252,12 @@ struct ...@@ -252,7 +252,12 @@ struct
match v1, v2 with match v1, v2 with
| None, None -> None | None, None -> None
| Some x, None | (Some _ | None), Some x -> Some x | Some x, None | (Some _ | None), Some x -> Some x
in { in
(* There is no need to preserve the uniqueness of ration stamps here, as
keys will always be given new stamps before the merge of identical keys.
This invariant depends on the sequence of operations performed by
the iterator and the trace_partitioning. *)
{
ration_stamp = None; ration_stamp = None;
branches = branches =
Extlib.list_first_n policy.history_size ( Extlib.list_first_n policy.history_size (
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment