anchor.diff:  
   add_all_backtracks_trace(_Transition, _ClockVector, _PreBound, [_] = Init, Acc) ->
       lists:reverse(Acc, Init);
  -add_all_backtracks_trace(Transition, ClockVector, PreBound, [StateI|Trace], Acc) ->
  -    #trace_state{i = I, last = {ProcSI, _} = SI, preemptions = Preemptions} = StateI,
  -    case Preemptions + 1 =< PreBound of
  -        true ->
  -            Clock = lookup_clock_value(ProcSI, ClockVector),
  -            case I > Clock andalso dependent(Transition, SI) of
  -                false ->
  -                    add_all_backtracks_trace(Transition, ClockVector, PreBound,
  -                                             Trace, [StateI|Acc]);
  -                true ->
  -                    ?f_debug("~4w: ~p ~p Clock ~p\n",
  -                             [I, dependent(Transition, SI), SI, Clock]),
  -                    [#trace_state{enabled = Enabled,
  -                                  backtrack = Backtrack,
  -                                  sleep_set = SleepSet} =
  -                         PreSI|Rest] = Trace,
  -                    Candidates = ordsets:subtract(Enabled, SleepSet),
  -                    %% Initial = find_initial(I, Acc),
  -                    %% ?f_debug("Initial: ~w\n",[ordsets:del_element(ProcSI, Initial)]),
  -                    case pick_from_E(Candidates, I, ClockVector) of
  -                        {ok, P} ->
  -                            NewBacktrack = ordsets:add_element(P, Backtrack),
  -                            ?f_debug("     Global adds: ~w\n", [P]),
  -                            NewPreSI =
  -                                PreSI#trace_state{backtrack = NewBacktrack},
  -                            lists:reverse(Acc, [StateI,NewPreSI|Rest]);
  -                        none ->
  -                            ?f_debug("     All sleeping... continue\n"),
  -                            #trace_state{clock_map = ClockMap} = StateI,
  -                            NewClockVector = lookup_clock(ProcSI, ClockMap),
  -                            add_all_backtracks_trace(Transition, NewClockVector,
  -                                                     PreBound, Trace, [StateI|Acc])
  -                    end
  -            end;
  -        false ->
  -            add_all_backtracks_trace(Transition, ClockVector, PreBound, Trace, [StateI|Acc])
  +add_all_backtracks_trace(Transition, ClockVector, PreBound,
  +                         [StateI|Trace], Acc) ->
  +    #trace_state{i = I, last = {ProcSI, _} = SI,
  +                 preemptions = Preemptions} = StateI,
  +    Action =
  +        case Preemptions + 1 =< PreBound of
  +            true ->
  +                Clock = lookup_clock_value(ProcSI, ClockVector),
  +                case I > Clock andalso dependent(Transition, SI) of
  +                    false -> {continue, ClockVector};
  +                    true ->
  +                        ?f_debug("~4w: ~p ~p Clock ~p\n",
  +                                 [I, dependent(Transition, SI), SI, Clock]),
  +                        [#trace_state{enabled = Enabled,
  +                                      backtrack = Backtrack,
  +                                      sleep_set = SleepSet} =
  +                             PreSI|Rest] = Trace,
  +                        Candidates = ordsets:subtract(Enabled, SleepSet),
  +                        %% Initial = find_initial(I, Acc),
  +                        %% ?f_debug("Initial: ~w\n",
  +                        %%          [ordsets:del_element(ProcSI, Initial)]),
  +                        case pick_from_E(Candidates, I, ClockVector) of
  +                            {ok, P} ->
  +                                NewBacktrack =
  +                                    ordsets:add_element(P, Backtrack),
  +                                ?f_debug("     Global adds: ~w\n", [P]),
  +                                NewPreSI =
  +                                    PreSI#trace_state{backtrack = NewBacktrack},
  +                                {done,
  +                                 lists:reverse(Acc, [StateI,NewPreSI|Rest])};
  +                            none ->
  +                                ?f_debug("     All sleeping... continue\n"),
  +                                #trace_state{clock_map = ClockMap} = StateI,
  +                                NewClockVector = lookup_clock(ProcSI, ClockMap),
  +                                {continue, NewClockVector}
  +                        end
  +                end;
  +            false ->
  +                {continue, ClockVector}
  +        end,
  +    case Action of
  +        {continue, UpdClockVector} ->
  +            add_all_backtracks_trace(Transition, UpdClockVector, PreBound,
  +                                     Trace, [StateI|Acc]);
  +        {done, FinalTrace} ->
  +            FinalTrace
       end.
   
   lookup_clock(P, ClockMap) ->
  
positive.code:     Variables = handle_instruction_op(Transition),
      handle_instruction_al(Transition, TraceTop, Variables).
  
  handle_instruction_op({Lid, {Spawn, _Info}}) when Spawn =:= spawn; Spawn =:= spawn_link ->
      ParentLid = Lid,
      ChildLid =
          receive
              %% This is the replaced message
              #sched{msg = spawned, lid = ParentLid, misc = ChildLid0, type = prev} ->
                  ChildLid0
          end,
      ChildNextInstr = wait_next(ChildLid, init),
  
negative.code: 	    {ok, {SelectedLid, Instruction}, NewState}
      end.
  
  replay_trace(#dpor_state{proc_before = ProcBefore} = State) ->
      ?f_debug("\nReplay is required...\n"),
      [#trace_state{lid_trace = LidTrace}|_] = State#dpor_state.trace,
  