docs: def load_array_elements(self, array, start_idx, no_of_elements):
          """
          Loads either a single element or a range of elements from the array.
  
          :param array:           Reference to the array.
          :param start_idx:       Starting index for the load.
          :param no_of_elements:  Number of elements to load.
  
          """
          # concretize start index
          concrete_start_idxes = self.concretize_load_idx(start_idx)
  
          if len(concrete_start_idxes) == 1:
              # only one start index
              # => concrete load
              concrete_start_idx = concrete_start_idxes[0]
              load_values = [self._load_array_element_from_heap(array, idx)
                             for idx in range(concrete_start_idx, concrete_start_idx+no_of_elements)]
              # if the index was symbolic before concretization, this
              # constraint it to concrete start idx
              self.state.solver.add(start_idx == concrete_start_idx)
  
          else:
              # multiple start indexes
              # => symbolic load
  
              # start with load values for the first concrete index
              concrete_start_idx = concrete_start_idxes[0]
              load_values = [self._load_array_element_from_heap(array, idx)
                             for idx in range(concrete_start_idx, concrete_start_idx+no_of_elements)]
              start_idx_options = [concrete_start_idx == start_idx]
  
              # update load values with all remaining start indexes
              for concrete_start_idx in concrete_start_idxes[1:]:
                  # load values for this start index
                  values = [self._load_array_element_from_heap(array, idx)
                            for idx in range(concrete_start_idx, concrete_start_idx+no_of_elements)]
                  # update load values with the new ones
                  for i, value in enumerate(values):
                      # condition every value with the start idx
                      # => if concrete_start_idx == start_idx
                      #    then use new value
                      #    else use the current value
                      load_values[i] = self.state.solver.If(
                          concrete_start_idx == start_idx,
                          value,
                          load_values[i]
                      )
                  start_idx_options.append(start_idx == concrete_start_idx)
  
              # constraint start_idx, s.t. it evals to one of the concretized indexes
              constraint_on_start_idx = self.state.solver.Or(*start_idx_options)
              self.state.add_constraints(constraint_on_start_idx)
  
          return load_values