def get_concat_level_bits(i, n):
  """Returns the bits of multiplying the current variable by the i-th index of the previous one.

  Take in integers i and n, returns a string containing the smt2 concat
  operation combining the bits of the multiplication of the current variable
  by the i-th index of the previous variable.
  Args:
  i: An integer, the index of the previous variable
  n: An integer, the number of bits in each bitvector
  """
  concats = []
  if i > 0:
    concats.append(f"(concat m{i}_{i} #b{'0' * i})")
  else:
    concats.append("m0_0")
  if i < (n - 1):
    for j in range(i + 1, n):
      rhs = concats[j - i - 1]
      concat = ["(concat", f"m{i}_{j}", rhs + ")"]
      concats.append(" ".join(concat))
  return concats[-1]