let jump (jumping: jumping) : choice_point option =
  Counter.inc jumping.split_counter;

  if not (Config.jumping jumping.config) then begin
    None
  end

  (* only check once in a while *)
  else if ((Counter.value jumping.split_counter) mod Const.jumping_check_every_splits) != 0 then begin
    None
  end

  else begin
    let jump_target =
      if Config.time_out_CPU jumping.config = 0.0 then begin
        (* no timeout given, just jump so often *)
        find_default_jump_target jumping
      end
      else begin
        (* jump based on the time left *)
        find_resource_jump_target jumping
      end
    in
      (* jump target found? *)
      match jump_target with
        | None ->
            (* no, no jump *)
            None

        | Some jump_target ->
            (* yes, but if this jump will leave us within an incomplete branch
               just jump so much farther, that we live the incomplete branch.
               after all, we want to find a model. *)
            let jump_target =
              match jumping.bound#dropped_choice_point with
                | None ->
                    jump_target

                | Some other ->
                    if State.compare_age jump_target other > 0 then
                      other
                    else
                      jump_target
            in

            let guiding_path =
              compute_guiding_path jumping.state jump_target
            in
              (* new path to the end *)
              jumping.guiding_paths <- jumping.guiding_paths @ [guiding_path];
              
              Statistic.inc_jump jumping.statistic;
(*              print_endline (guiding_path_to_string guiding_path);*)
              
              Some jump_target
  end