code: def write_word_at(self, index: int, value: Union[int, BitVec, bool, Bool]) -> None:
          
          try:
              # Attempt to concretize value
              if isinstance(value, bool):
                  _bytes = (
                      int(1).to_bytes(32, byteorder="big")
                      if value
                      else int(0).to_bytes(32, byteorder="big")
                  )
              else:
                  _bytes = util.concrete_int_to_bytes(value)
              assert len(_bytes) == 32
              self[index : index + 32] = list(bytearray(_bytes))
          except (Z3Exception, AttributeError):  # BitVector or BoolRef
              value = cast(Union[BitVec, Bool], value)
              if isinstance(value, Bool):
                  value_to_write = If(
                      value,
                      symbol_factory.BitVecVal(1, 256),
                      symbol_factory.BitVecVal(0, 256),
                  )
              else:
                  value_to_write = value
              assert value_to_write.size() == 256
  
              for i in range(0, value_to_write.size(), 8):
                  self[index + 31 - (i // 8)] = Extract(i + 7, i, value_to_write)
docs: Writes a 32 byte word to memory at the specified index`
  
          :param index: index to write to
          :param value: the value to write to memory