anchor.diff:  wait_for_exit([]) -> ok;
   wait_for_exit([P|Rest]) ->
       receive {'EXIT', P, _Reason} -> wait_for_exit(Rest) end.
  -
   
   %%%----------------------------------------------------------------------
   %%% Instrumentation interface
  
positive.code: handle_instruction_al(_Transition, TraceTop, {}) ->
      TraceTop.
  
  max_cv(D1, D2) ->
      Merger = fun(_Key, V1, V2) -> max(V1, V2) end,
      orddict:merge(Merger, D1, D2).
  
  update_named_sends(Name, PLid, Nexts) ->
      Map =
          fun(Lid, Instr) ->
  
negative.code: new_backtrack(LidList) ->
      [{Lid, Tr, []} || {Lid, Tr} <- LidList].
  
  %% -----------------------------------------------------------------------------
  %% The main explore routine
  %% -----------------------------------------------------------------------------
  
  explore(State) ->
      receive
          stop_analysis -> dpor_return(State)
      after 0 ->
          case select_from_backtrack(State) of
              {ok, {Lid, Cmd, _} = Selected, UpdState} ->
                  case Cmd of
                      {error, _ErrorInfo} ->
                          RaceCheckState = race_check(UpdState),
                          ErrorState = report_error(Selected, RaceCheckState),
                          NewState = drop_last_frame(ErrorState),
                          explore(NewState);
                      _Else ->
                          ?debug("Plan: ~p\n",[Selected]),
                          Next = wait_next(Lid, Cmd),
                          NextState = update_trace(Selected, Next, UpdState),
                          NewState = add_some_next_to_backtrack(NextState),
                          explore(NewState)
                  end;
              none ->
                  UpdState =
                      case State#dpor_state.must_replay of
                          true ->
                              %% Already backtracking
                              State;
                          false ->
                              RaceCheckState = race_check(State),
                              report_possible_deadlock(RaceCheckState)
                      end,
                  NewState = drop_last_frame(UpdState),
                  case finished(NewState) of
                      false -> explore(NewState);
                      true -> dpor_return(NewState)
                  end
          end
      end.
  
  %% -----------------------------------------------------------------------------
  
  select_from_backtrack(#dpor_state{trace = []}) -> none;
  select_from_backtrack(#dpor_state{must_replay = MustReplay,
  				  trace = Trace} = State) ->
      [#trace_state{backtrack = Backtrack, done = Done} = _TraceTop|_] = Trace,
      ?debug("------------\nExplore ~p\n------------\n",
             [_TraceTop#trace_state.i + 1]),
      case pick_from_backtrack(Backtrack, Done) of
          none ->
              ?debug("Backtrack set explored\n",[]),
              none;
          {true, SelectedLid} ->
              UpdState =
                  case MustReplay of
                      true -> replay_trace(State);
                      false -> State
                  end,
              [NewTraceTop|RestTrace] = UpdState#dpor_state.trace,
              Instruction =
                  dict:fetch(SelectedLid, NewTraceTop#trace_state.nexts),
              NewDone = ordsets:add_element(SelectedLid, Done),
              FinalTraceTop =
                  NewTraceTop#trace_state{done = NewDone},
              FinalState = UpdState#dpor_state{trace = [FinalTraceTop|RestTrace]},
              {ok, Instruction, FinalState}
      end.
  
  pick_from_backtrack([], _) -> none;
  pick_from_backtrack([{B, _, _}|Rest], Done) ->
      case ordsets:is_element(B, Done) of
          true  -> pick_from_backtrack(Rest, Done);
          false -> {true, B}
      end.
  
  %% -----------------------------------------------------------------------------
  
  %% - add new entry with new entry
  %% - wait any possible additional messages
  %% - check for async
  update_trace(Selected, Next, State) ->
      #dpor_state{trace = Trace, dpor_flavor = Flavor} = State,
      NewTrace = update_trace(Selected, Next, Trace, Flavor, false),
      State#dpor_state{trace = NewTrace}.
  
  update_trace({Lid, _, _} = Selected, Next, [PrevTraceTop|_] = Trace,
               Flavor, Replaying) ->
      #trace_state{i = I, enabled = Enabled, blocked = Blocked,
                   pollable = Pollable, done = Done, backtrack = Backtrack,
                   nexts = Nexts, clock_map = ClockMap, sleep_set = SleepSet,
                   preemptions = Preemptions, last = {LLid,_,_}} = PrevTraceTop,
      Expected = dict:fetch(Lid, Nexts),
      NewNexts = dict:store(Lid, Next, Nexts),
      ClockVector = lookup_clock(Lid, ClockMap),
      MaybeNotPollable = ordsets:del_element(Lid, Pollable),
      {NewPollable, NewEnabled, NewBlocked} =
          update_lid_enabled(Lid, Next, MaybeNotPollable, Enabled, Blocked),
      CommonNewTraceTop =
          case Replaying of
              false ->
                  NewN = I+1,
                  BaseClockVector = orddict:store(Lid, NewN, ClockVector),
                  LidsClockVector =
                      recent_dependency_cv(Selected, BaseClockVector, Trace),
                  NewClockMap = dict:store(Lid, LidsClockVector, ClockMap),
                  NewPreemptions =
                      case ordsets:is_element(LLid, Enabled) of
                          true ->
                              case Lid =:= LLid of
                                  false -> Preemptions + 1;
                                  true -> Preemptions
                              end;
                          false -> Preemptions
                      end,
                  NewSleepSetCandidates =
                      ordsets:union(ordsets:del_element(Lid, Done), SleepSet),
                  #trace_state{
                     i = NewN, last = Selected, nexts = NewNexts,
                     enabled = NewEnabled, sleep_set = NewSleepSetCandidates,
                     blocked = NewBlocked, clock_map = NewClockMap,
                     pollable = NewPollable, preemptions = NewPreemptions};
              {true, ReplayTop} ->
                  ReplayTop#trace_state{
                    last = Selected, nexts = NewNexts, pollable = NewPollable}
          end,
      InstrNewTraceTop = check_external_changes(CommonNewTraceTop),
      UpdTraceTop =
          #trace_state{last = UpdSelected,
                       sleep_set = UpdSleepSet,
                       nexts = UpdNexts,
                       backtrack = TempBacktrack} =
          update_instr_info(Lid, Selected, InstrNewTraceTop),
      PrevTrace =
          case UpdSelected =:= Expected of
              true -> Trace;
              false ->
                  rewrite_while_awaked(UpdSelected, Expected, Trace)
          end,
      FinalTraceTop =
          case Replaying of
              false ->
                  ?debug("Happened before: ~p\n",
                         [orddict:to_list(
                            begin
                                CMM = UpdTraceTop#trace_state.clock_map,
                                CCC = lookup_clock(Lid, CMM),
                                case lookup_clock_value(Lid, ClockVector) of
                                    0 -> orddict:erase(Lid, CCC);
                                    QQ -> orddict:store(Lid, QQ, CCC)
                                end
                            end)]),
                  ?debug("Selected: ~P\n", [UpdSelected, ?DEBUG_DEPTH]),
                  {NewSleepSet, NewAwaked} =
                      case Flavor =:= 'none' of
                          true -> {[], []};
                          false ->
                              filter_awaked(UpdSleepSet, UpdNexts, UpdSelected)
                      end,
                  NewBacktrack =
                      case TempBacktrack =:= [] of
                          true ->
                              case {Next, Selected} of
                                  {_, {_, { halt, _}, _}} -> [];
                                  {{_, {error, _}, _}, _} ->
                                      new_backtrack([{Lid, Next}]);
                                  _Else ->
                                      element(3, lists:keyfind(Lid, 1, Backtrack))
                              end;
                          false -> TempBacktrack
                      end,
                  NewLastBlocked = ordsets:is_element(Lid, NewBlocked),
                  ?debug("Awaked: ~p\n", [NewAwaked]),
                  UpdTraceTop#trace_state{
                    last_blocked = NewLastBlocked,
                    backtrack = NewBacktrack,
                    sleep_set = NewSleepSet,
                    awaked = NewAwaked};
              {true, _ReplayTop} ->
                  UpdTraceTop
          end,
      [FinalTraceTop|PrevTrace].
  
  update_lid_enabled(Lid, {_, Next, _}, Pollable, Enabled, Blocked) ->
      {NewEnabled, NewBlocked} =
          case is_enabled(Next) of
              true -> {Enabled, Blocked};
              false ->
                  {ordsets:del_element(Lid, Enabled),
                   ordsets:add_element(Lid, Blocked)}
          end,
      NewPollable =
          case is_pollable(Next) of
              false -> Pollable;
              true -> ordsets:add_element(Lid, Pollable)
          end,
      {NewPollable, NewEnabled, NewBlocked}.
  
  is_enabled({'receive', blocked}) -> false;
  is_enabled(_Else) -> true.
  
  is_pollable({'receive', blocked}) -> true;
  is_pollable({'after', _Info}) -> true;
  is_pollable(_Else) -> false.
  
  recent_dependency_cv(Transition, ClockVector, Trace) ->
      Fun =
          fun(#trace_state{
              last = {Lid, _, _} = Transition2,
              clock_map = CM}, CVAcc) ->
                  case concuerror_deps:dependent(Transition, Transition2) of
                      true ->
                          CV = lookup_clock(Lid, CM),
                          max_cv(CVAcc, CV);
                      false -> CVAcc
                  end
          end,
      lists:foldl(Fun, ClockVector, Trace).
  
  %% Handle instruction is broken in two parts to reuse code in replay.
  handle_instruction(Transition, TraceTop) ->
      {NewTransition, Extra} = handle_instruction_op(Transition),
      handle_instruction_al(NewTransition, TraceTop, Extra).
  
  check_external_changes(TraceTop) ->
      case unexpected_exits(TraceTop) of
          {true, NewTraceTop} -> NewTraceTop;
          none ->
              #trace_state{pollable = Pollable} = TraceTop,
              PollableList = ordsets:to_list(Pollable),
              lists:foldl(fun poll_all/2, TraceTop, PollableList)
      end.
  
  unexpected_exits(#trace_state{nexts = Nexts} = TraceTop) ->
      receive
          {'DOWN', _, process, _, normal} -> unexpected_exits(TraceTop);
          {'DOWN', _, process, Pid, Reason} ->
              ?debug("Unexpected exit: ~p ~p\n", [Pid, Reason]),
              Lid = lid_from_pid(Pid),
              Entry = {Lid, {error, [exit, Reason, []]}, []},
              NewNexts = dict:store(Lid, Entry, Nexts),
              {true, TraceTop#trace_state{nexts = NewNexts,
                                          backtrack = [{Lid, Entry, []}]
                                         }}
      after
          0 -> none
      end.
  
  poll_all(Lid, TraceTop) ->
      case poll(Lid) of
          {'receive', Info} = Res when
                Info =:= unblocked;
                Info =:= had_after ->
              #trace_state{pollable = Pollable,
                           blocked = Blocked,
                           enabled = Enabled,
                           %% TODO: Remove next line
                           sleep_set = SleepSet,
                           nexts = Nexts} = TraceTop,
              NewPollable = ordsets:del_element(Lid, Pollable),
              NewBlocked = ordsets:del_element(Lid, Blocked),
              NewSleepSet = ordsets:del_element(Lid, SleepSet),
              NewEnabled = ordsets:add_element(Lid, Enabled),
              {Lid, _Old, Msgs} = dict:fetch(Lid, Nexts),
              NewNexts = dict:store(Lid, {Lid, Res, Msgs}, Nexts),
              TraceTop#trace_state{pollable = NewPollable,
                                   blocked = NewBlocked,
                                   enabled = NewEnabled,
                                   sleep_set = NewSleepSet,
                                   nexts = NewNexts};
          _Else ->
              TraceTop
      end.
  
  update_instr_info(Lid, Selected, CommonNewTraceTop) ->
      IntermediateTraceTop = handle_instruction(Selected, CommonNewTraceTop),
      UpdatedClockVector =
          lookup_clock(Lid, IntermediateTraceTop#trace_state.clock_map),
      {Lid, RewrittenInstr, _Msgs} = IntermediateTraceTop#trace_state.last,
      Messages = orddict:from_list(replace_messages(Lid, UpdatedClockVector)),
      IntermediateTraceTop#trace_state{last = {Lid, RewrittenInstr, Messages}}.
  
  filter_awaked(SleepSet, Nexts, Selected) ->
      Filter =
          fun(Lid) ->
                  Instr = dict:fetch(Lid, Nexts),
                  Dep = concuerror_deps:dependent(Instr, Selected),
                  ?debug(" vs ~p: ~p\n",[Instr, Dep]),
                  not Dep
          end,
      {A, NA} = lists:partition(Filter, SleepSet),
      {ordsets:from_list(A), ordsets:from_list(NA)}.
  
  rewrite_while_awaked(Transition, Original, Trace) ->
      rewrite_while_awaked(Transition, Original, Trace, []).
  
  rewrite_while_awaked(_Transition, _Original, [], Acc) -> lists:reverse(Acc);
  rewrite_while_awaked({P, _, _} = Transition, Original,
                       [TraceTop|Rest] = Trace, Acc) ->
      #trace_state{sleep_set = SleepSet,
                   nexts = Nexts} = TraceTop,
      case
          not ordsets:is_element(P, SleepSet) andalso
          {ok, Original} =:= dict:find(P, Nexts)
      of
          true ->
              NewNexts = dict:store(P, Transition, Nexts),
              NewTraceTop = TraceTop#trace_state{nexts = NewNexts},
              rewrite_while_awaked(Transition, Original, Rest, [NewTraceTop|Acc]);
          false ->
              lists:reverse(Acc, Trace)
      end.
  
  %% -----------------------------------------------------------------------------
  %% Dpor logic
  %% -----------------------------------------------------------------------------
  
  race_check(#dpor_state{preemption_bound = Bound, trace = Trace,
  			       dpor_flavor = Flavor} = State) ->
      case Flavor of
          none ->
              %% add_some_next will take care of all the backtracks.
              State;
          _ ->
              NewTrace = race_check(Trace, Bound, Flavor),
              State#dpor_state{trace = NewTrace}
      end.
  
  race_check(Trace, PreBound, Flavor) ->
      race_check(Trace, [], PreBound, Flavor).
  
  race_check([_] = Trace, _Rest, _PreBound, _Flavor) -> Trace;
  race_check([#trace_state{race_checked = true}|_] = Trace,
             _Rest, _PreBound, Flavor)
    when Flavor =:= ?CLASSIC; Flavor =:= ?SOURCE ->
      Trace;
  race_check(Trace, Rest, PreBound, Flavor) ->
      [#trace_state{i = _I, last = {Lid, _, _} = Transition} = Top|
       [#trace_state{clock_map = ClockMap}|_] = PTrace] = Trace,
      NewPTrace = race_check(PTrace, [Top|Rest], PreBound, Flavor),
      NewTop = Top#trace_state{race_checked = true},
      ?debug("Race check: ~p ~p\n", [_I, Transition]),
      case concuerror_deps:may_have_dependencies(Transition) of
          true ->
              ClockVector = lookup_clock(Lid, ClockMap),
              add_all_backtracks_trace(Transition, Lid, ClockVector, PreBound,
                                       Flavor, NewPTrace, [NewTop], Rest);
          false -> [NewTop|NewPTrace]
      end.
  
  add_all_backtracks_trace(_Transition, _Lid, _ClockVector, _PreBound,
                           _Flavor, [_] = Init, Acc, _Rest) ->
      lists:reverse(Acc, Init);
  add_all_backtracks_trace(Transition, Lid, ClockVector, PreBound, Flavor,
                           [#trace_state{preemptions = Preempt} = StateI|Trace],
                           Acc, Rest)
    when Preempt + 1 > PreBound, PreBound =/= ?INFINITY ->
      add_all_backtracks_trace(Transition, Lid, ClockVector, PreBound, Flavor,
                               Trace, [StateI|Acc], Rest);
  add_all_backtracks_trace(Transition, Lid, ClockVector, PreBound, Flavor,
                           [StateI,PreSI|Rest], Acc, AccRest) ->
      #trace_state{i = I, last = {ProcSI, _, _} = SI} = StateI,
      Clock = lookup_clock_value(ProcSI, ClockVector),
      Action =
          case I > Clock andalso concuerror_deps:dependent(Transition, SI) of
              false -> {continue, PreSI};
              true ->
                  ?debug("~4w: ~P Clock ~p\n", [I, SI, ?DEBUG_DEPTH, Clock]),
                  #trace_state{enabled = Enabled,
                               backtrack = Backtrack,
                               done = Done,
                               sleep_set = SleepSet} = PreSI,
                  Sleepers = ordsets:union(SleepSet, Done),
                  case Flavor of
                      ?FULL ->
                          Result =
                              find_path([StateI|Acc], AccRest, ProcSI, I,
                                        Sleepers, Backtrack),
                          case Result of
                              inversion_explored ->
                                  ?debug("    Inversion is explored...\n"),
                                  {continue, PreSI};
                              equivalent_scheduled ->
                                  ?debug("    Equivalent is scheduled...\n"),
                                  {continue, PreSI};
                              {replace, NewBacktrack} ->
                                  ?debug("    NewBacktrack: ~p\n",[NewBacktrack]),
                                  {continue,
                                   PreSI#trace_state{backtrack = NewBacktrack}}
                          end;
                      ?SOURCE ->
                          Candidates = ordsets:subtract(Enabled, Sleepers),
                          BacktrackSet =
                              ordsets:from_list([P || {P, _, _} <- Backtrack]),
                          case find_initials(BacktrackSet, Candidates, I, Acc) of
                              equivalent_scheduled ->
                                  ?debug("    Equivalent is scheduled...\n"),
                                  {done, PreSI};
                              inversion_explored ->
                                  ?debug("    Inversion is explored...\n"),
                                  {continue, PreSI};
                              {add, P} ->
                                  NewBacktrack = Backtrack ++ [{P, dummy, []}],
                                  ?debug("    NewBacktrack: ~p\n",[NewBacktrack]),
                                  {continue,
                                   PreSI#trace_state{backtrack = NewBacktrack}}
                          end;
                      ?CLASSIC ->
                          throw(temporarily_unavailable)
                  end
          end,
      case Action of
          {continue, NewPreSI} ->
              add_all_backtracks_trace(Transition, Lid, ClockVector, PreBound,
                                       Flavor, [NewPreSI|Rest], [StateI|Acc],
                                       AccRest);
          {done, NewPreSI} ->
              lists:reverse([StateI|Acc], [NewPreSI|Rest])
      end.
  
  %% -----------------
  %% For optimal DPOR:
  %% -----------------
  
  find_path([#trace_state{nexts = Nexts}|Acc],
            Rest, ProcSI, I, Sleepers, Backtrack) ->
      SleepSet = ordsets:del_element(ProcSI, Sleepers),
      Annotated = [{P, dict:fetch(P, Nexts)} || P <- SleepSet],
      NotDeps = not_deps(Acc, Rest, ProcSI, I),
      ?debug("      NotDeps:~p\n",[NotDeps]),
      try
          case find_weak_initial(NotDeps, Annotated) of
              {true, _, _} -> throw(inversion_explored);
              false ->
                  Pred = fun({P,_,_}) -> P =/= ProcSI end,
                  {Done, [{ProcSI,_,_} = Current|Future]} =
                      lists:splitwith(Pred, Backtrack),
                  ?debug("      Future:~p\n",[Future]),
                  NewFuture = insert_best_match(Future, NotDeps),
                  {replace, Done ++ [Current|NewFuture]}
          end
      catch
          throw:Reason -> Reason
      end.
  
  find_weak_initial(    _,    []) -> false;
  find_weak_initial(Trace, [C|R]) ->
      case find_weak_initial(Trace, [C], []) of
          false -> find_weak_initial(Trace, R);
          True -> True
      end.
  
  find_weak_initial(_, [], _) -> false;
  find_weak_initial([], [{Lid, _}|_], Acc) ->
      {true, Lid, lists:reverse(Acc)};
  find_weak_initial([{Lid, _, _} = Tr|Rest], Candidates, Acc) ->
      case lists:keyfind(Lid, 1, Candidates) of
          {Lid, _} -> {true, Lid, lists:reverse(Acc, Rest)};
          false ->
              Pred = fun({_, Tr2}) -> not concuerror_deps:dependent(Tr, Tr2) end,
              NewCandidates = lists:filter(Pred, Candidates),
              find_weak_initial(Rest, NewCandidates, [Tr|Acc])
      end.
  
  insert_best_match([], Trace) ->
      Fold = fun({P, _,_} = Tr, PAcc) -> [{P, Tr, PAcc}] end,
      lists:foldl(Fold, [], lists:reverse(Trace));
  insert_best_match(Backtrack, Trace) ->
      ?debug("      Trace:~p\n", [Trace]),
      Ps = [{P,Tr} || {P,Tr,_} <- Backtrack],
      case find_weak_initial(Trace, Ps) of
          {true, Lid, NewTrace} ->
              ?debug("      WeakIni:~p\n", [Lid]),
              {Lid, Tr, Further} = lists:keyfind(Lid, 1, Backtrack),
              ?debug("      Further:~p\n",[Further]),
              case Further =:= [] of
                  true -> throw(equivalent_scheduled);
                  false ->
                      NewFuther = insert_best_match(Further, NewTrace),
                      lists:keyreplace(Lid, 1, Backtrack, {Lid, Tr, NewFuther})
              end;
          false ->
              Backtrack ++ insert_best_match([], Trace)
      end.
  
  not_deps(Acc, Rest, ProcSI, I) ->
      not_deps(Acc, Rest, ProcSI, I, []).
  
  not_deps([], no_rest, _, _, Path) ->
      lists:reverse(Path);
  not_deps([#trace_state{last = Last}], Rest, ProcSI, I, Path)
    when Rest =/= no_rest ->
      not_deps(Rest, no_rest, ProcSI, I, [Last|Path]);
  not_deps([#trace_state{last = {Lid, _, _} = Last, clock_map = ClockMap}|Acc],
           Rest, ProcSI, I, Path) ->
      Lid2Clock = lookup_clock(Lid, ClockMap),
      NewPath =
          case lookup_clock_value(ProcSI, Lid2Clock) >= I of
              true  -> Path;
              false -> [Last|Path]
          end,
      not_deps(Acc, Rest, ProcSI, I, NewPath).
  
  %% --------------------------
  %% For source set based DPOR:
  %% --------------------------
  
  find_initials(Backtrack, Candidates, I, Trace) ->
      ?debug("    BT:~p\n    C :~p\n", [Backtrack, Candidates]),
      find_initials(Trace, Backtrack, Candidates, I, none).
  
  find_initials(_Trace, _Backtrack, [], _I, MaybePred) ->
      case MaybePred of
          none -> inversion_explored;
          {true, Lid} -> {add, Lid}
      end;
  find_initials([#trace_state{last = {Lid, _, _}}],
                Backtrack, Candidates, _I, MaybePred) ->
      case MaybePred of
          none ->
              case ordsets:is_element(Lid, Candidates) of
                  false -> inversion_explored;
                  true ->
                      case ordsets:is_element(Lid, Backtrack) of
                          true -> equivalent_scheduled;
                          false -> {add, Lid}
                      end
              end;
          {true, Lid2} -> {add, Lid2}
      end;
  find_initials([#trace_state{i = _J,
                              last = {Lid, _, _}, clock_map = ClockMap}|Trace],
                Backtrack, Candidates, I, MaybePred) ->
      case ordsets:is_element(Lid, Candidates) of
          false ->
              find_initials(Trace, Backtrack, Candidates, I, MaybePred);
          true ->
              NewCands = ordsets:del_element(Lid, Candidates),
              LidVector = lookup_clock(Lid, ClockMap),
              ?debug("     ~p: ~p ~p\n", [_J, Lid, LidVector]),
              Fold = fun({L, V}, Acc) -> Acc andalso (L =:= Lid orelse V < I) end,
              case lists:foldl(Fold, true, LidVector) of
                  false ->
                      find_initials(Trace, Backtrack, NewCands, I, MaybePred);
                  true ->
                      case {ordsets:is_element(Lid, Backtrack), MaybePred} of
                          {true,    _} -> equivalent_scheduled;
                          {   _, none} ->
                              find_initials(Trace, Backtrack, NewCands,
                                            I, {true, Lid});
                          _ ->
                              find_initials(Trace, Backtrack, NewCands,
                                            I, MaybePred)
                      end
              end
      end.
  
  %% --------------------------------------
  %% Manipulating the clock vectors / maps:
  %% --------------------------------------
  
  empty_clock_map() -> dict:new().
  
  lookup_clock(P, ClockMap) ->
      case dict:find(P, ClockMap) of
          {ok, Clock} -> Clock;
          error -> orddict:new()
      end.
  
  lookup_clock_value(P, CV) ->
      case orddict:find(P, CV) of
          {ok, Value} -> Value;
          error -> 0
      end.
  
  max_cv(D1, D2) ->
      Merger = fun(_Key, V1, V2) -> max(V1, V2) end,
      orddict:merge(Merger, D1, D2).
  
  %% -----------------------------------------------------------------------------
  
  add_some_next_to_backtrack(State) ->
      #dpor_state{trace = [TraceTop|Rest], dpor_flavor = Flavor,
                  preemption_bound = PreBound} = State,
      #trace_state{enabled = Enabled, sleep_set = SleepSet,
                   backtrack = OldBacktrack, last = {Lid, _, _},
                   preemptions = Preemptions, nexts = Nexts} = TraceTop,
      ?debug("Pick next: Enabled: ~p Sleeping: ~p\n", [Enabled, SleepSet]),
      Backtrack =
          case OldBacktrack =:= [] of
              true ->
                  Set =
                      case Flavor of
                          'none' ->
                              case ordsets:is_element(Lid, Enabled) of
                                  true when Preemptions =:= PreBound -> [Lid];
                                  _Else -> Enabled
                              end;
                          _Other ->
                              case ordsets:subtract(Enabled, SleepSet) of
                                  [] -> [];
                                  [H|_] = Candidates ->
                                      case ordsets:is_element(Lid, Candidates) of
                                          true -> [Lid];
                                          false -> [H]
                                      end
                              end
                      end,
                  Annotated = [{P, dict:fetch(P, Nexts)} || P <- Set],
                  new_backtrack(Annotated);
              false ->
                  ?debug("Predefined: ~p\n", [OldBacktrack]),
                  [A || {K, _, _} = A <- OldBacktrack,
                        not ordsets:is_element(K, SleepSet)]
          end,
      ?debug("Picked: ~p\n",[Backtrack]),
      NewTraceTop = TraceTop#trace_state{backtrack = Backtrack},
      State#dpor_state{trace = [NewTraceTop|Rest]}.
  
  %% -----------------------------------------------------------------------------
  
  report_error(Transition, State) ->
      #dpor_state{trace = Trace, tickets = Tickets} = State,
      ?debug("ERROR!\n~P\n",[Transition, ?DEBUG_DEPTH]),
      Error = convert_error_info(Transition),
      LidTrace = convert_trace_to_error_trace(Trace, [Transition]),
      Ticket = create_ticket(Error, LidTrace),
      %% Report the error to the progress logger.
      concuerror_log:progress({'error', Ticket}),
      State#dpor_state{must_replay = true, tickets = [Ticket|Tickets]}.
  
  report_possible_deadlock(#dpor_state{trace = []} = State) -> State;
  report_possible_deadlock(State) ->
      #dpor_state{trace = [TraceTop|_] = Trace, tickets = Tickets,
                  sleep_blocked_count = SBlocked} = State,
      {NewTickets, NewSBlocked} =
          case TraceTop#trace_state.enabled of
              [] ->
                  case TraceTop#trace_state.blocked of
                      [] ->
                          ?debug("NORMAL!\n"),
                          {Tickets, SBlocked};
                      Blocked ->
                          ?debug("DEADLOCK!\n"),
                          Error = {deadlock, Blocked},
                          LidTrace = convert_trace_to_error_trace(Trace, []),
                          Ticket = create_ticket(Error, LidTrace),
                          %% Report error
                          concuerror_log:progress({'error', Ticket}),
                          {[Ticket|Tickets], SBlocked}
                  end;
              _Else ->
                  case TraceTop#trace_state.sleep_set =/= []
                      andalso TraceTop#trace_state.done =:= [] of
                      false ->
                          {Tickets, SBlocked};
                      true ->
                          ?debug("SLEEP SET BLOCK\n"),
                          {Tickets, SBlocked+1}
                  end
          end,
      State#dpor_state{must_replay = true, tickets = NewTickets,
                       sleep_blocked_count = NewSBlocked}.
  
  convert_trace_to_error_trace([], Acc) -> Acc;
  convert_trace_to_error_trace([#trace_state{
                                   last = {Lid, _, _} = Entry,
                                   last_blocked = Blocked}|Rest], Acc) ->
      NewAcc =
          [Entry|
           case Blocked of
               false -> Acc;
               true -> [{Lid, block, []}|Acc]
           end],
      convert_trace_to_error_trace(Rest, NewAcc).
  
  create_ticket(Error, LidTrace) ->
      InitTr = init_tr(),
      [{P1, init, []} = InitTr|Trace] = LidTrace,
      InitSet = sets:add_element(P1, sets:new()),
      {ErrorState, _Procs} =
          lists:mapfoldl(fun convert_error_trace/2, InitSet, Trace),
      concuerror_ticket:new(Error, ErrorState).
  
  convert_error_trace({Lid, {error, [ErrorOrThrow,Kind|_]}, _Msgs}, Procs)
    when ErrorOrThrow =:= error; ErrorOrThrow =:= throw ->
      Msg =
          concuerror_error:type(concuerror_error:new({Kind, foo})),
      {{exit, Lid, Msg}, Procs};
  convert_error_trace({Lid, block, []}, Procs) ->
      {{block, Lid}, Procs};
  convert_error_trace({Lid, {Instr, Extra}, _Msgs}, Procs) ->
      NewProcs =
          case Instr of
              Spawn when Spawn =:= spawn; Spawn =:= spawn_link;
                         Spawn =:= spawn_monitor; Spawn =:= spawn_opt ->
                  NewLid =
                      case Extra of
                          {Lid0, _MonLid} -> Lid0;
                          Lid0 -> Lid0
                      end,
                  sets:add_element(NewLid, Procs);
              exit   -> sets:del_element(Lid, Procs);
              _ -> Procs
          end,
      NewInstr =
          case Instr of
              send ->
                  {Orig, Dest, Msg} = Extra,
                  NewDest =
                      case is_atom(Orig) of
                          true -> {name, Orig};
                          false -> check_lid_liveness(Dest, NewProcs)
                      end,
                  {send, Lid, NewDest, Msg};
              'receive' ->
                  {_Tag, Origin, Msg} = Extra,
                  {'receive', Lid, Origin, Msg};
              'after' ->
                  {'after', Lid};
              is_process_alive ->
                  {is_process_alive, Lid, check_lid_liveness(Extra, NewProcs)};
              TwoArg when TwoArg =:= register;
                          TwoArg =:= whereis ->
                  {Name, TLid} = Extra,
                  {TwoArg, Lid, Name, check_lid_liveness(TLid, NewProcs)};
              process_flag ->
                  {trap_exit, Value, _Links} = Extra,
                  {process_flag, Lid, trap_exit, Value};
              exit ->
                  {exit, Lid, normal};
              exit_2 ->
                  {Lid2, Reason} = Extra,
                  {exit_2, Lid, Lid2, Reason};
              send_after ->
                  {Lid2, Msg} = Extra,
                  {send_after, Lid, Lid2, Msg};
              start_timer ->
                  {Lid2, Msg} = Extra,
                  {start_timer, Lid, Lid2, Msg};
              PortOp when PortOp =:= port_command;
                          PortOp =:= port_control ->
                  {PortOp, Lid, Extra};
              Monitor when Monitor =:= monitor;
                           Monitor =:= spawn_monitor ->
                  {TLid, _RefLid} = Extra,
                  {Monitor, Lid, check_lid_liveness(TLid, NewProcs)};
              ets ->
                  case Extra of
                      {insert, [_EtsLid, Tid, _K, _KP, Objects, _Status]} ->
                          {ets_insert, Lid, {Tid, Objects}};
                      {insert_new, [_EtsLid, Tid, _K, _KP, Objects, _Status]} ->
                          {ets_insert_new, Lid, {Tid, Objects}};
                      {delete, [_EtsLid, Tid]} ->
                          {ets_delete, Lid, Tid};
                      {C, [_EtsLid | Options]} ->
                          ListC = atom_to_list(C),
                          AtomC = list_to_atom("ets_" ++ ListC),
                          {AtomC, Lid, list_to_tuple(Options)}
                  end;
              _ ->
                  {Instr, Lid, Extra}
          end,
      {NewInstr, NewProcs}.
  
  
  check_lid_liveness(not_found, _Live) ->
      not_found;
  check_lid_liveness(Lid, Live) ->
      case sets:is_element(Lid, Live) of
          true -> Lid;
          false -> {dead, Lid}
      end.
  
  convert_error_info({_Lid, {error, [Kind, Type, Stacktrace]}, _Msgs})->
      NewType =
          case Kind of
              error -> Type;
              throw -> {nocatch, Type};
              exit -> Type
          end,
      {Tag, Details} = concuerror_error:new({NewType, foo}),
      Info =
          case Tag of
              exception -> {NewType, Stacktrace};
              assertion_violation -> Details
          end,
      {Tag, Info}.
  
  %% -----------------------------------------------------------------------------
  
  drop_last_frame(#dpor_state{trace = []} = State) -> State;
  drop_last_frame(#dpor_state{trace = [_|Trace]} = State) ->
      State#dpor_state{trace = Trace}.
  
  finished(#dpor_state{trace = Trace}) ->
      Trace =:= [].
  
  dpor_return(State) ->
      %% First clean up the last interleaving
      GroupLeader = State#dpor_state.group_leader,
      Output = concuerror_io_server:group_leader_sync(GroupLeader),
      case State#dpor_state.show_output of
          true  -> io:put_chars(Output);
          false -> ok
      end,
      ProcBefore = State#dpor_state.proc_before,
      proc_cleanup(processes() -- ProcBefore),
      %% Return the analysis result
      RunCnt = State#dpor_state.run_count,
      SBlocked = State#dpor_state.sleep_blocked_count,
      case State#dpor_state.tickets of
          [] -> {ok, RunCnt, SBlocked};
          Tickets -> {error, RunCnt, SBlocked, Tickets}
      end.
  
  %% =============================================================================
  %% ENGINE (manipulation of the Erlang processes under the scheduler)
  %% =============================================================================
  
  start_target_op(Target) ->
      concuerror_lid:start(),
      %% Initialize a new group leader
  